# HG changeset patch
# User urbanc
# Date 1158672164 -7200
# Node ID 56e4bb01fd9976baea879a579c98d6d257888446
# Parent  9dba9c7872c9ceec453c7db3f995f4b2526fec86
tuned

diff -r 9dba9c7872c9 -r 56e4bb01fd99 src/HOL/Nominal/INSTALL
--- 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/
+