Chapter 3

The Structure of the Mizar Article

3.1 The Whole Structure

Next, we will explain the structure of an article. An article consists of two parts, the environ and main sections. The environ section starts with environ and ends with a semicolon. The main section starts with begin and ends with a semicolon. However, we can also divide a main section into some parts by inserting several "begin"s. This is equivalent to dividing into a paragraph in a paper. If the name of a paragraph is written to the .BIB file which we explain later, when an article is automatically changed into the form of the general mathematics paper later, the name of a paragraph will be written in a begin position.