These internal formats describe block structured proofs in the ILF standard proof format . The outermost block is dummy . It contains a block article which has a subblock for each selected Mizar article and at the end a block containing the declarations. The blocks describing Mizar articles contain the selected definitions and theorems. They may have attached further subblocks containing their justifications.
Some declarations come with subblocks which collect relevant properties of the declared concepts.
In order to understand the meaning of the items in the database it is strongly suggested to request a LaTeX version of the corresponding WWW page from the ILF Mathematical Library . The ILF Mathematical Library is developed by Thomas Bauer , Ingo Dahn , Thomas Honigmann , and Christoph Wernhard . It is based on a pre-processing of Mizar articles developed by Czeslaw Bylinski for this purpose. The tools used for proof presentation are also used by the ILF Mail Server . Its language is not documented.