This is a snapshot of the ASCII database file "set.mm" (contained in the
Metamath program download). For
efficiency, the proofs in set.mm are typically stored in a compressed
format that is hard for humans to read directly. (But if you want to
try, the precise specification of the compressed format is given in
Appendix B, p. 137, of the Metamath
book.) The Metamath program is used to work with the proofs and can
display them in several different ways, such as the web page 2eu5, which was generated with the command
"show statement 2eu5 /html". The markup syntax for symbols and
cross-reference links in comments is described under the Metamath
program commands "help language" and "help html".
Notes The
monospaced font in the editor screen is 8-point Andale Mono. The KEDIT
editor is a product of the Mansfield Software Group. The syntax
coloring is specified by a file called mm.kld, which is placed in
KEDIT's USER directory.
* MM.KLD - KEDIT Language Definition for .mm (Metamath) files
:case
respect
:identifier
[a-zA-Z0-9${}.=] [a-zA-Z0-9${}.=]
:comment
paired $( $) nonest
:keyword
${ ALTERNATE 9
$} ALTERNATE 9
$d ALTERNATE 1
$p ALTERNATE 1
$v ALTERNATE 1
$= ALTERNATE 1
$. ALTERNATE 1
$a ALTERNATE 1
$e ALTERNATE 1
$f ALTERNATE 1
$c ALTERNATE 1
|
This page was last updated on
30-Nov-2004.
Metamath