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: cd [ISABELLE_HOME] ./configure 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 type: ./build More object-logics can be made similarly: ./build FOL HOL Running the system ------------------ Provided that compilation was successful, you can now run something like: [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 somewhere else -- or they just won't work! $Id$