Isabelle installation notes

 ===========================

 1) System installation

 ----------------------

 The Isabelle distribution includes both complete sources and

 precompiled binary packages for common Unix platforms.

 Quick installation

 ------------------

 Ready-to-go packages are provided for the ML compiler and runtime

 system, the Isabelle sources, and some major object-logics.  A minimal

 site installation of Isabelle on Linux/x86 works like this:

   tar -C /usr/local -xzf Isabelle.tar.gz

   tar -C /usr/local -xzf polyml_x86-linux.tar.gz

   tar -C /usr/local -xzf HOL_x86-linux.tar.gz

 The install prefix given above may be changed as appropriate.  By

 default the ML system (and other contributed packages) are expected in

 any of the following locations:

   1) [ISABELLE_HOME]/contrib

   2) [ISABELLE_HOME]/..

   4) /usr/local

   3) /usr/share

   5) /opt

 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.

 The installation may be finished as follows:

   cd [ISABELLE_HOME]

   ./bin/isatool install -p /usr/local/bin

 The install utility creates global references to the present Isabelle

 installation, enabling users to invoke the Isabelle executables

 without explicit path names.  Incidently, this is the only place where

 a static reference to [ISABELLE_HOME] is created; thus isatool install

 has to be run again whenever the Isabelle distribution is moved later.

 Compiling logics

 ----------------

 The Isabelle.tar.gz archive already contains all Isabelle sources (and

 documentation).  Precompiled object-logics are provided for

 convenience.

 Assuming proper configuration of the underlying ML system

 (cf. Isabelle's etc/settings), further object-logics may be compiled

 like this:

   [ISABELLE_HOME]/build FOL

 Special object-logic targets may be specified as follows:

   [ISABELLE_HOME]/build -m HOL-Algebra HOL

 2) User installation

 --------------------

 Running the Isabelle binaries

 -----------------------------

 Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)

 directly from their location within the distribution directory

 [ISABELLE_HOME] like this:

   [ISABELLE_HOME]/bin/isabelle HOL

 This starts an interactive Isabelle session within the current text

 terminal.  [ISABELLE_HOME]/bin may be put into the shell's search

 PATH.  An alternative is to create global references to the Isabelle

 executables as follows:

   [ISABELLE_HOME]/bin/isatool install -p ~/bin

 Note that the site-wide Isabelle installation may already provide

 Isabelle executables in some global bin directory (such as

 /usr/local/bin).

 $Id$