| Preface |
|
| Concerning the Revised Edition |
|
|
|
|
| 1 |
A Summary of Mizar |
|
|
|
|
| 2 |
An Outline of the Mizar Language |
|
|
|
|
| 3 |
The Structure of the Mizar Article |
|
|
3.1 |
The Structure of the Mizar |
|
|
3.2 |
The Environ Section |
|
|
|
3.2.1 |
Vocabulary Section |
|
|
|
3.2.2 |
Notation Section，Constructors Section |
|
|
|
3.2.3 |
Requirements Section |
|
|
|
3.2.4 |
Definitions Section |
|
|
|
3.2.5 |
Theorems Section |
|
|
|
3.2.6 |
Schemes Section |
|
|
3.3 |
The Main Section |
|
|
|
3.3.1 |
Sentences |
|
|
|
3.3.2 |
Theorem |
|
|
|
|
|
|
| 4 |
Method for Demonstration |
|
|
4.1 |
Basic Method for Demonstration |
|
|
4.2 |
Irrational Method |
|
|
4.3 |
Dividing the Demonstrations |
|
|
4.4 |
Demonstration of the Equivalence |
|
|
4.5 |
Method for Using Now |
|
|
|
4.5.1 |
Caution About End |
|
|
4.6 |
All Symbols |
|
|
|
4.6.1 |
When There Are Two Variables |
|
|
|
4.6.2 |
Method for Writing With such that |
|
|
|
4.6.3 |
Division of Sentences |
|
|
|
4.6.4 |
Dividing Sentences With Assume |
|
|
|
4.6.5 |
Caution Following that |
|
|
4.7 |
Existing Symbols |
|
|
|
4.7.1 |
Method for Using Consider |
|
|
|
4.7.2 |
Method for Using Given |
|
|
4.8 |
Dividing Into Cases |
|
|
|
4.8.1 |
Premise for Dividing Into Cases |
|
|
|
4.8.2 |
Labels for Dividing Into Labels |
|
|
|
4.8.3 |
Warning About Labels |
|
|
4.9 |
Method for Using @proof |
|
|
4.10 |
Introduction of New Variable (Set, reconsider) |
|
|
4.11 |
About Take |
|
|
4.12 |
Hereby |
|
|
|
|
|
|
| 5 |
About Mode |
|
|
5.1 |
Mode |
|
|
5.2 |
Structure Level |
|
|
5.3 |
Mode change |
|
|
5.4 |
Declaration of Mode During a Demonstration |
|
|
|
5.4.1 |
Warning About c= |
|
|
|
5.4.2 |
Example of Actually Using a Definition |
|
|
|
|
|
|
| 6 |
Definition |
|
|
6.1 |
Definition |
|
|
6.2 |
Method for Writing the Vocabulary File |
|
|
6.3 |
Predicate Definition |
|
|
6.4 |
Functor Definition |
|
|
6.5 |
Method for Using Equals |
|
|
6.6 |
Mode Definition |
|
|
6.7 |
Cluster Definition |
|
|
6.8 |
Introduction of structure |
|
|
|
|
|
|
| 7 |
Practice Environment |
|
|
7.1 |
Installation |
|
|
|
7.1.1 |
MS-DOS Version |
|
|
|
7.1.2 |
Linux Version |
|
|
7.2 |
Preparation for Using Mizar |
|
|
7.3 |
Mizar System |
|
|
7.4 |
The Mizar Usage |
|
|
|
7.4.1 |
Accommodate |
|
|
|
7.4.2 |
Mizar Checker |
|
|
|
7.4.3 |
When There Is An Error |
|
|
|
7.4.4 |
Useful Command |
|
|
|
|
|
|
| 8 |
Registering to the Library |
|
|
8.1 |
Improvement of an Article |
|
|
|
8.1.1 |
Improvement of the Main Section |
|
|
|
8.1.2 |
Checking the Environ Section |
|
|
8.2 |
Preparation for Registration |
|
|
|
|
|
|
| 9 |
Useful tools |
|
|
9.1 |
To find VOC files containing a terminology (findvoc) |
|
|
9.2 |
To check the contents of the VOC file |
|
|
9.3 |
To serach for the ABS file which the terminology appears |
|
|
|
9.3.1 |
Method for Using grep |
|
|
|
9.3.2 |
Method for serach on the Web |
|
|
|
|
|
|
| 10 |
About the version upgrade |
|
|
|
|
|
|
| A |
List of Reserved Words |
|
|
|
|
|
|
| B |
A Compilation of Mizar Library Theorems |
|
|
B.1 |
TARSKI |
|
|
B.2 |
AXIOMS |
|
|
B.3 |
BOOLE |
|
|
B.4 |
XBOOL_0 |
|
|
B.5 |
XBOOL_1 |
|
|
B.6 |
REAL_1 |
|
|
B.7 |
NAT_1 |
|
|
B.8 |
FUNCT_1 |
|
|
B.9 |
SUBSET_1 |
|
|
B.10 |
FINSEQ_1 |
|
|
B.11 |
FUNCT_2 |
|
|
B.12 |
SQUARE_1 |
|
|
B.13 |
REAL_2 |
|
|
|
|
|
|
| C |
C.1 |
Contacting the Mizar Society |
|
|
|
C.1.1 |
Mizar Society |
|
|
|
C.1.2 |
Mizar Society Nagano Circle |
|
|
C.2 |
Acquisition of Mizar by ftp |
|
|
C.3 |
How to submit Articles via the Internet |
|
|
C.4 |
WWW Homepage |
|
|
C.5 |
Formalized Mathematics |
|
|
|
|
|
|
| Conclusion |
|
| Reference |
|