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/isabelle 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/