author oheimb
Mon, 21 Sep 1998 23:04:51 +0200
changeset 5519 54e313ed22ba
parent 5396 cfc1fe0b8490
child 6258 1f85c03fb3df
permissions -rw-r--r--
re-added mem and list_all improved indentation improved addbefore and addSbefore improved mechanism for unsafe wrappers

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