* Pure now provides its own version of intro/elim/dest attributes;
useful for building new logics, but beware of confusion with the
Provers/classical ones!
* HOL: removed "case_split" thm binding, should use "cases" proof
method anyway;
* tuned syntax of "induct" method;
* new "cases" method for propositions, inductive sets and types;
* HOL/records: admit "r" as field name;
Isabelle compilation and 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
This does not store any references to [ISABELLE_HOME]. You may safely
move the system later, without running ./configure again.
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 anywhere else, or
they just won't work! If you really feel the urge to install
independent Isabelle binaries anywhere else do it like this:
[ISABELLE_HOME]/bin/isatool install -p /usr/local/bin
$Id$