author nipkow
Thu, 26 Nov 1998 12:18:08 +0100
changeset 5974 6acf3ff0f486
parent 5396 cfc1fe0b8490
child 6258 1f85c03fb3df
permissions -rw-r--r--
Added filter_prems_tac

Isabelle installation notes

Unpacking the archive

After unpacking the Isabelle distribution archive (using tar and gzip)
you are left with some directory IsabelleYY-X. You may install this
anywhere, but please just *not* as ~/isabelle!!!

The place where you put the contents of IsabelleYY-X will be referred
to as [ISABELLE_HOME] subsequently.

Auto configuration

There are some minor adaptions to be made of the Isabelle distribution
to your system environment. Simply type:


ML system settings and compilation

Before actual compilation you have to tell Isabelle about your
Standard ML system.  These settings reside in ./etc/settings, which
may be also overridden by ~/isabelle/etc/settings. There are already
various sample configurations in ./etc/settings commented out.

To build the core Isabelle/Pure and the default object-logic, just


More object-logics can be made similarly:

  ./build FOL HOL

Running the system

Provided that compilation was successful, you can now run something

  [ISABELLE_HOME]/bin/isabelle FOL

This starts an interactive Isabelle session within your current text
terminal.  You may want to put [ISABELLE_HOME]/bin into your shell's
search PATH.

Please do *not* copy (or link) the Isabelle scripts anywhere else --
or they just won't work!  If you really feel the urge to install
independent Isabelle binaries somewhere you should rather do it like

  [ISABELLE_HOME]/bin/isatool install /usr/local/bin