--- a/README Tue May 20 19:29:50 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
- 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 lambda@ahl.co.uk.
-
-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 sml-nj@research.bell-labs.com.
-
-
- 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 isabelle-users@cl.cam.ac.uk provides a forum
-for Isabelle users to discuss problems and exchange information. To join,
-send a message to isabelle-users-request@cl.cam.ac.uk.
-
-------------------------------------------------------------------------------
-
-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: lcp@cl.cam.ac.uk
-Computer Laboratory Phone: +44-223-334600
-University of Cambridge Fax: +44-223-334748
-Pembroke Street
-Cambridge CB2 3QG
-England
-
-Tobias Nipkow E-mail: nipkow@informatik.tu-muenchen.de
-Institut für Informatik Phone: +49-89-2105-2690
-T. U. München Fax: +49-89-2105-8183
-D-80290 München
-Germany
-
-$Id$