[Top] [Contents] [Index] [ ? ]

Emacs Authoring Environment for Mizar

This file documents version 1.98 of Mizar Mode, an Emacs authoring environment for the Mizar system.

Mizar Mode 1.98 has been tested with GNU Emacs 21.2 and Windows port of GNU Emacs 21.2.

1. Prerequisities  
2. Basic Functions  
3. Summaries and Hide/Show  
4. Running Mizar utilities  
5. Miscellaneous editing  
6. Browsing Functions  
7. Grepping in MML  
8. Miscellaneous Emacs facilities for fast mizaring  
9. Constructor explanations  
10. MML Query  
11. Mizar Proof Advisor  
12. MoMM  
13. Proof Skeletons  
14. Mizar TWiki  
Function and Command Index  
Variable and User Option Index  
Keystroke Index  
Concept Index  
-- The Detailed Node Listing ---
Prerequisities
1.1 Installation  
1.2 Emacs basics  
Installation
1.1.1 XEmacs compatibility  
Basic Functions
2.1 Running Mizar  
2.2 Indentation and commenting  
2.3 Error explanations and movement  
Summaries and Hide/Show
3.1 Hide/Show - Hiding proofs  
Running Mizar utilities
4.1 Simple constructor and vocabulary utilities  
4.2 Irrelevant Utilities  
4.3 Other Utilities  
Simple constructor and vocabulary utilities
4.1.1 Constructors and user symbols  
Miscellaneous editing
5.1 Proof checking  
5.2 Then placement  
Miscellaneous Emacs facilities for fast mizaring
8.1 Imenu and Speedbar support  
8.2 Abbreviations  
Constructor explanations
9.1 How Constructor explanations work  
9.2 Getting Constructor explanations  
9.3 Using Constructor explanations  
MML Query
10.1 Asking arbitrary queries  
MoMM
12.1 Installing MoMM  
12.2 Starting MoMM in Mizar Mode  
12.3 Getting MoMM hints  



This document was generated by Josef Urban on December, 12 2004 using texi2html