This package contains the metamath program and several Metamath
databases.


Copyright
---------

The metamath program is copyright under the terms of the GNU GPL license
version 2 or later.  See the file LICENSE.TXT in this directory.

Individual databases (*.mm files) are either public domain or under
the GNU GPL, as indicated by comments in their headers.

See http://us.metamath.org/copyright.html for further license and
copyright information that applies to the content of this package.


Instructions
------------

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

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

Note:  In Linux, if the Backspace key doesn't delete characters typed
after the "MM>" prompt, try adding this line to your ~/.bash_profile
file:

  stty echoe echok echoctl echoke

(This will also fix the same problem with other command-line programs
such as ftp.  The problem was observed with the default installation of
Debian Woody when connected to via ssh from Cygwin.  The problem did not
occur with the default installation of RedHat 7.2.)


Optional user interface enhancement
------------------------------------

On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use
if you run it inside of rlwrap:

  http://utopia.knoware.nl/~hlub/uck/software/

which provides up-arrow command history and other command-line editing
features.  After you install rlwrap per its instructions, invoke the
Metamath program with "rlwrap ./metamath set.mm".

(The Windows version of the Metamath program was compiled with lcc,
which has similar features built-in.)


Windows Compilation
-------------------

To reproduce the included metamath.exe for Windows, use lcc-win32
version 3.8, with the following command:

  lc -O m*.c -o metamath.exe


Further suggestions
-------------------

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
------------

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


List of databases
-----------------

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)
  big-unifier.mm - A unification stress test (see comments in the file).
  peano.mm - A nicely commented presentation of Peano arithmetic, written
      by Robert Solovay (unlike the ones above, this database is NOT public
      domain but is copyright under the terms of the GNU GPL license)