# HG changeset patch
# User urbanc
# Date 1149166484 -7200
# Node ID 489e6be0b19d5be770aa60e1cd98fb22dc21acc5
# Parent  b345d4e70ca9edd6c4476c203563e8acd5b1ef64
added some installation notes for the nominal package

diff -r b345d4e70ca9 -r 489e6be0b19d src/HOL/Nominal/INSTALL
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nominal/INSTALL	Thu Jun 01 14:54:44 2006 +0200
@@ -0,0 +1,37 @@
+
+Installation Notes for the Nominal Datatype Package
+===================================================
+
+The nominal datatype package is part of the development
+snapshots of Isabelle. Get the sources from
+
+    http://isabelle.in.tum.de/devel/
+
+Follow the instructions in INSTALL for 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
+
+The sources 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 including the Proof-General interface can be started
+
+  Isabelle -L HOL-Nominal <<theory file to be opened>> &
+
+This automatically loads the correct keyword file needed
+for the nominal datatype package.