[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