INSTALL

Added the following lemmas tp Divides and a few others to Arith and NatDef:

div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend

Fixed a broken proof in WF_Rel.ML. No idea what caused this.

+
−
+
−***************************************************************************
+
−
+
−IMPORTANT NOTE: This file describes the *new* installation procedure
+
−using various scripts that are still supposed beta for Isabelle94-8.
+
−If you encounter serious problems, you may want to consider compiling
+
−Isabelle the olden way, as described in README.old.
+
−
+
−***************************************************************************
+
−
+
−
+
−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$