--- a/src/HOL/Nominal/INSTALL Wed Jun 09 16:23:00 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-
-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/
-