For Unix/Linux/MacOSX, compile with the command "gcc *.c -o metamath",
then type "./metamath set.mm" to run.

For Windows, click on "metamath.exe" and type "read set.mm".

Once in the program, use the "help" command to guide you.  For more
information, see the Metamath book available at http://metamath.org .

To uninstall, just delete the "metamath" directory - nothing else
(Registry, etc.) is touched in your system.

The data base files included are:
  set.mm - logic and set theory database (see Ch. 3 of the Metamath book);
      the Metamath Proof Explorer pages were generated from this database.
  ql.mm - quantum logic database; the Quantum Logic Explorer pages were
      generated from this database.
  demo0.mm - demo of simple formal system (see Ch. 2 of the Metamath book)
  miu.mm - Hofstadter's MIU-system (see Appendix D of the Metamath book)
  peano.mm - A nicely commented presentation of Peano arithmetic, written
      by Robert Solovay

Note:  If there is a binary file called "metamath" in this directory, it
was compiled for a specific Linux/Unix/MacOSX operating system and may
not run on your system.  Please compile it again per the instructions at
the top of this file, before trying to run it.