removed;
authorwenzelm
Fri, 20 Jun 1997 11:37:53 +0200
changeset 3454 40b1287347d7
parent 3453 b2ecba22b8be
child 3455 fbd4eb0cd0da
removed;
NEWS
README.old
--- a/NEWS	Fri Jun 20 11:34:05 1997 +0200
+++ b/NEWS	Fri Jun 20 11:37:53 1997 +0200
@@ -2,6 +2,12 @@
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
+New in Isabelle???? (DATE ????)
+-------------------------------
+
+* removed old README and Makefiles;
+
+
 New in Isabelle94-8 (May 1997)
 ------------------------------
 
--- a/README.old	Fri Jun 20 11:34:05 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,164 +0,0 @@
-
-***************************************************************************
-
-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 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$