7.4 The Mizar Usage

7.4.1 Accommodate

For instance, let us assume that an article named EXAMPLE1.MIZ was created. This file is set on a directory called TEXT under one's own directories created by 7.2. First, we accommodate it (accommodate means to gather files and adjust them). In order to accommodate, at the command prompt, we set EXAMPLE1.MIZ as an argument and enter a command called ACCOM as follows.


    An argument must be taken as a file name (here EXAMPLE1.MIZ) including a path. This accommodation reads the environ section in and gets ready for the article's proof by making some files of the referred article's theorems, definitions, and others that are needed by an article. Sometimes, errors may appear at this point when, for example, names of an abstract file are written incorrectly in the environ section.
    Accommodation does not need to be carried out every time; however, when the environ section is changed, it needs to be accommodated again.