Package mizar-mode-1:7.12.01-4.166.1132-1

(For more information on Mizar, see http://www.mizar.org) The Emacs authoring environment for Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority of) Mizar authors. Mizar is a non-programmable and non-tactical verifier; proofs are developed in the traditional `write-compile-correct' software programming loop. While this method is in the beginning more laborious than the methods employed in tactical and programmable proof assistants, it makes the `proof code' in the long-run more readable, maintainable and reusable. This seems to be a crucial factor for a long-term and large-scale formalization effort. MizarMode has been designed to facilitate this kind of proof development by a number of `code-generating', `code-browsing' and `code-searching' methods or tools programmed or integrated within it. These methods and tools now include e.g. the automated generation of proof skeletons, proof advice using trained machine learning tools like Mizar Proof Advisor or deductive tools like MoMM, semantic browsing of the articles and abstracts, structured viewing, etc. (Adapted from the abstract to "MizarMode - Integrated Proof Assistance Tools for the Mizar Way of Formalizing Mathematics", by Josef Urban, available at http://kti.ms.mff.cuni.cz/~urban/mizmode.ps .)

To get started, simply add the forms (autoload 'mizar-mode "mizar" "Major mode for editing Mizar articles." t) (autoload 'mmlquery-decode "mizar") (autoload 'mmlquery-mode "mizar") to your emacs initialization file. To configure emacs to turn on mizar-mode whenever a Mizar file is loaded, add the forms (setq auto-mode-alist (append '( ("\\.miz" . mizar-mode) ("\\.abs" . mizar-mode)) auto-mode-alist)) to your emacs initialization file. Add the form (setq format-alist (append '( "::[ \t]*Content-[Tt]ype:[ ]*text/mmlquery" mmlquery-decode nil nil mmlquery-mode)) format-alist) if you would like to use the MML Query feature (for more information about MML query, see http://mmlquery.mizar.org). In any case, the main entry point into the system is the command `mizar-mode'; type the key sequence M-x mizar-mode to being structually editing Mizar code. Finally, consider using the abbreviations defined in /sw/share/doc/mizar-mode/abbrev_defs; they may make editing Mizar texts easier.