--- a/src/HOL/Nominal/INSTALL Tue Sep 19 15:22:35 2006 +0200
+++ b/src/HOL/Nominal/INSTALL Tue Sep 19 15:22:44 2006 +0200
@@ -2,9 +2,10 @@
Installation Notes for the Nominal Datatype Package
===================================================
-Although the nominal datatype package is now officially
-part of the development snapshot of Isabelle, we keep
-a semi-official nominal snapshot under
+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/
@@ -22,6 +23,9 @@
./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
@@ -34,9 +38,20 @@
Starting Isabelle with the Nominal Datatype Package Preloaded
=============================================================
-Isabelle including the Proof-General interface can be started
+Isabelle and the Proof-General interface can be started
+with
Isabelle -L HOL-Nominal <<theory file to be opened>> &
-This automatically loads the correct keyword file needed
-for the nominal datatype package.
+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/
+