Mizar Article


Mizar-Article   =  
 Text-Proper   .


Mizar Article can be considered as an extremely detailed mathematical text, written in the fixed formal language. Usually, its source is a text file which name is equipped with an obligatory extension .miz. The goal of writing a Mizar Article is to prove some claims and to introduce some new notions, based on the facts and concepts built in the Mizar System or gathered in a library.

Each Mizar Article consists of two parts. In the Environment Declaration the information of what should be imported from the library is specified. Text Proper contains theorems and definitions.

The division of a Mizar Article into two parts has one more technical meaning. Those two parts of a Mizar Article are processed by two different programs:


Relevant errors

See also

Home | Index of Syntax Items

Last modified: November 21, 2007