README.old

+
+***************************************************************************
+
+IMPORTANT NOTE: This is the old README. The installation procedure
+described below basically still works for Isabelle94-8, but will be
+phased out next time.
+
+***************************************************************************
+
+
+
+		     ISABELLE-94 DISTRIBUTION DIRECTORY
+
+------------------------------------------------------------------------------
+ISABELLE-94 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
+DOCUMENTATION.  
+
+In particular, theory files are no longer forced into lower case, but must
+be identical to the actual theory name.  See the script
+conv-theory-files.pl on directory Tools.
+------------------------------------------------------------------------------
+
+This directory contains the complete Isabelle system.  To build and test
+all the Isabelle object-logics, use the shell script make-all (on directory
+Tools).  Pure Isabelle and each of the object-logics can be built
+separately using the Makefiles in the respective directories; read them for
+more information.
+
+			HOW TO BUILD ISABELLE
+
+Here are brief instructions.  For more detail, read further.
+
+1.  Create a directory to hold the Isabelle executable images.
+    Set the environment variable ISABELLEBIN to its full (absolute) pathname.
+
+2.  Set the environment variable ISABELLECOMP to the command to execute your
+    Standard ML compiler.
+
+3.  If using Poly/ML, set the environment variable ML_DBASE to the full 
+    pathname of the empty Poly/ML database.
+
+4.  Change your working directory to that containing this file.
+
+5a. To build ALL logics and run examples, type "make-all" and wait up to 
+    10 hours.  Standard ML of New Jersey will require up to 200M
+    of disc space!  Poly/ML will require about 25M.
+
+-OR-
+5b. To build ALL logics but run no examples, type "make-all -notest".  This
+    is much faster than 5a but needs just as much disc space.
+
+-OR-
+5c. To build just one logic, such as HOL, change to directory HOL and type
+    "make" or "make test".  This may trigger further Makes automatically.
+
+
+			SUITABLE ML COMPILERS
+
+You can use two different Standard ML compilers: Poly/ML version 2.03 or later
+(from Abstract Hardware Ltd) and Standard ML of New Jersey (Version 0.93 or
+later).  Poly/ML is a commercial product and costs money, but it is stable and
+efficient; moreover its database system is convenient for interactive work.
+SML/NJ needs lots of store and disc space, but it is free.  Some recent
+versions of SML/NJ are significantly faster than 0.93, but beware of many
+incompatibilities among them; you might be forced to edit the file
+Pure/NJ1xx.ML.  VERSIONS BETWEEN 109.16 AND 109.21 ARE VERY SLOW.
+
+To obtain Poly/ML, contact Abstract Hardware Ltd, The Howell Building, Brunel
+University, Uxbridge UB8 3PH, England, email [e-mail].
+
+To obtain Standard ML of New Jersey, see the Web page 
+	http://cm.bell-labs.com/cm/cs/what/smlnj/software.html
+or send email to [e-mail].
+
+
+			ENVIRONMENT VARIABLES
+
+The Makefiles and make-all use environment variables that you should set
+according to your site configuration.  See file Tools/make-all-nj for an
+example using the Bourne shell, sh.
+
+ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
+images.  This directory *must* be different from the Isabelle source
+directory.  ISABELLEBIN must be an absolute pathname (one starting with "/").
+
+ML_DBASE is an *absolute* pathname to the initial Poly/ML database.  It is not
+required for New Jersey ML.
+
+ISABELLECOMP is the command to run ML compiler, typically "/bin/sml" or "poly
+-noDisplay -h 15000".  (The -h switch to Poly specifies an initial heap
+allocation, which you should consider increasing if a command fails with the
+message "Run out of store".)  Please DO NOT use a command such as
+"sml @SMLdebug=/dev/null", since the pathname after "sml" will confuse the
+Makefiles. 
+
+If, after stripping a leading pathname, the compiler begins with the letters
+"poly" then the Makefiles assume Poly/ML.  If it begins with the letters "sml"
+then they assume Standard ML of New Jersey.
+
+
+			 STRUCTURE OF THIS DIRECTORY
+
+Important files include...
+  COPYRIGHT 	Copyright notice and Disclaimer of Warranty
+  Pure		contains source files for Pure Isabelle (no object-logic)
+  Provers	contains generic theorem provers: simplifier, etc.
+  Tools		contains shell scripts and utilities 
+
+The following subdirectories contain object-logics:
+  FOL 		natural deduction First-Order Logic 
+			(intuitionistic and classical versions)
+  FOLP 		First-Order Logic with Proof terms
+  ZF		Zermelo-Fraenkel set theory
+  HOL		Classical Higher-Order Logic
+  LCF		Logic for Computable Functions (domain theory) built upon FOL
+  HOLCF		A version of LCF built upon HOL
+  CTT		Constructive Type Theory
+  Sequents	Sequent calcul: first-order logic
+				modal logics T, S4, S43
+				intuitionistic linear logic
+  CCL		Martin Coen's Classical Computational Logic
+  Cube		Barendregt's Lambda Cube
+
+David Aspinall has written a user interface for Isabelle.  It runs under
+GNU Emacs.  It's useful to both novices and experts.  You can get it by ftp
+from ftp.dcs.ed.ac.uk, file /pub/da/Isamode.tar.gz.
+
+Object-logics include examples files in subdirectory ex or file ex.ML.
+These files can be loaded in batch mode.  The commands can also be
+executed interactively, using the windows on your workstation.  This is a
+good way to get started.
+
+Each object-logic is built on top of Pure Isabelle, and possibly on top of
+another object logic like FOL or HOL.  A database or binary called Pure is
+first created, then the object-logic is loaded on top.  Poly/ML extends
+Pure using its "make_database" operation.  Standard ML of New Jersey starts
+with the Pure core image and loads the object-logic's ROOT.ML.
+
+------------------------------------------------------------------------------
+
+The electronic mailing list [e-mail] provides a forum
+for Isabelle users to discuss problems and exchange information.  To join,
+send a message to [e-mail].
+
+------------------------------------------------------------------------------
+
+Please report any problems you encounter.  While we shall try to be helpful,
+we can accept no responsibility for the deficiences of Isabelle and their
+consequences.
+
+Lawrence C Paulson		E-mail: [e-mail]
+Computer Laboratory 		Phone: [phone]
+University of Cambridge 	Fax:   [phone] 
+Pembroke Street 
+Cambridge CB2 3QG 
+England
+
+Tobias Nipkow			E-mail: [e-mail]
+Institut für Informatik		Phone: [phone]
+T. U. München			Fax:   [phone]
+D-80290 München
+Germany
+
+$Id$