Mizar Article

Syntax

Mizar-Article   =  
 environ  
 Environment-Declaration  
begin  
 Text-Proper   .


Description

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:

Examples

Relevant errors

See also


Home | Index of Syntax Items

Last modified: November 21, 2007