src/HOL/Nominal/INSTALL

declare lex_prod_def [code del]

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/