# HG changeset patch
# User urbanc
# Date 1152008018 -7200
# Node ID d649506f40c3783d3b91227c12ca9ae4222a3113
# Parent  e4d50f8f37229e153cd2c4556eeaac3eed049237
updated

diff -r e4d50f8f3722 -r d649506f40c3 src/HOL/Nominal/INSTALL
--- a/src/HOL/Nominal/INSTALL	Tue Jul 04 11:36:08 2006 +0200
+++ b/src/HOL/Nominal/INSTALL	Tue Jul 04 12:13:38 2006 +0200
@@ -2,14 +2,19 @@
 Installation Notes for the Nominal Datatype Package
 ===================================================
 
-The nominal datatype package is part of the development
-snapshots of Isabelle. Get the sources from
+Although the nominal datatype package is now officially 
+part of the development snapshot of Isabelle, we keep 
+a semi-official nominal snapshot under
+
+  http://isabelle.in.tum.de/nominal/
 
-    http://isabelle.in.tum.de/devel/
+This snapshot contains the latest stable release of the
+nominal datatype package.
 
-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:
+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
 
@@ -17,8 +22,8 @@
 
    ./bin/isatool install -p /usr/local/bin
 
-The sources sources of the nominal datatype package
-can be found in the directory
+The sources of the nominal datatype package can be found 
+in the directory
 
     [ISABELLE_HOME]/src/HOL/Nominal