Installation Notes for the Nominal Datatype Package
===================================================
Although the nominal datatype package is an official
package in the development snapshot of Isabelle, we
keep a semi-official snapshot of Isabelle and Nominal
under
http://isabelle.in.tum.de/nominal/
This snapshot contains the latest stable release of the
nominal datatype package.
To install it, follow the instructions of Isabelle's INSTALL
about how a snap-shot can be set up. The building process
needs to be started inside the [ISABELLE_HOME] directory with
the command:
./build -m HOL-Nominal
After the build completes, install the files with the command
./bin/isatool install -p /usr/local/bin
where /usr/local/bin needs to be replaced by an appropriate
directory, if you are not root on the system.
The sources of the nominal datatype package can be found
in the directory
[ISABELLE_HOME]/src/HOL/Nominal
The examples are in
[ISABELLE_HOME]/src/HOL/Nominal/Examples
Starting Isabelle with the Nominal Datatype Package Preloaded
=============================================================
Isabelle and the Proof-General interface can be started
with
Isabelle -L HOL-Nominal <<theory file to be opened>> &
on the command-line. This automatically loads the correct
keyword file needed for the nominal datatype package.
Problems with starting Isabelle and Proof-General usually
come from old versions of Proof-General. So make sure you
have installed at least the version ProofGeneral-3.6pre050930.
If you have problems or comments about the installation process,
please make use of the nominal mailing list at
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/