deletion of obsolete/private files; update of README
authorlcp
Thu Oct 28 17:40:50 1993 +0100 (1993-10-28)
changeset 863406bd994306
parent 85 914270f33f2d
child 87 c378e56d4a4b
deletion of obsolete/private files; update of README
README
     1.1 --- a/README	Thu Oct 28 11:32:37 1993 +0100
     1.2 +++ b/README	Thu Oct 28 17:40:50 1993 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -		     ISABELLE-92 DISTRIBUTION DIRECTORY
     1.5 +		     ISABELLE-93 DISTRIBUTION DIRECTORY
     1.6  
     1.7  ------------------------------------------------------------------------------
     1.8 -ISABELLE-92 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
     1.9 +ISABELLE-93 IS INCOMPATIBLE WITH EARLIER VERSIONS.  PLEASE CONSULT THE
    1.10  DOCUMENTATION.
    1.11  ------------------------------------------------------------------------------
    1.12  
    1.13 @@ -13,8 +13,8 @@
    1.14  				THE MAKEFILES
    1.15  
    1.16  The Makefiles can use two different Standard ML compilers: Poly/ML version
    1.17 -1.88MSX or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
    1.18 -(Version 75 or later).  Poly/ML is a commercial product and costs money,
    1.19 +2.03 or later (from Abstract Hardware Ltd) and Standard ML of New Jersey
    1.20 +(Version 0.93 or later).  Poly/ML is a commercial product and costs money,
    1.21  but it is reliable and its database system is convenient for interactive
    1.22  work.  SML of New Jersey requires lots of memory and disc space, but it is
    1.23  free and its code sometimes runs faster.  Both compilers are perfectly
    1.24 @@ -33,7 +33,12 @@
    1.25  ISABELLECOMP is the ML compiler, typically "poly -noDisplay" or "sml".  If
    1.26  ISABELLECOMP begins with the letters "poly" then the Makefiles assume that
    1.27  it is Poly/ML; if it begins with the letters "sml" then they assume
    1.28 -Standard ML of New Jersey.
    1.29 +Standard ML of New Jersey.  
    1.30 +
    1.31 +If a Poly/ML session fails with the message "Run out of store" then you
    1.32 +have used up the entire heap.  If your tactic is not in a loop, allocating
    1.33 +more heap at startup should correct the problem.  For instance, "poly -h
    1.34 +15000" allocates sufficient heap space to rebuild all Isabelle examples.
    1.35  
    1.36  
    1.37  			 STRUCTURE OF THIS DIRECTORY
    1.38 @@ -41,16 +46,14 @@
    1.39  The directory Pure containes pure Isabelle, which has no object-logic.
    1.40  
    1.41  Other important files include...
    1.42 -    COPYRIGHT   	Copyright notice and Disclaimer of Warranty
    1.43 -    make-rulenames	shell script used during Make
    1.44 -    make-all		shell script for building entire system
    1.45 -    expandshort		shell script to expand "shortcuts" in files
    1.46 -    prove_goal.el       Emacs command to change proof format
    1.47 -    xlisten		shell script for running Isabelle under X
    1.48 -    teeinput		shell script to run Isabelle, logging inputs to a file
    1.49 -    theory-template.ML	template file for defining new theories
    1.50 -    Pure		directory of source files for Pure Isabelle
    1.51 -    Provers		directory of generic theorem provers
    1.52 +  COPYRIGHT   		Copyright notice and Disclaimer of Warranty
    1.53 +  make-all		shell script for building entire system
    1.54 +  expandshort		shell script to expand "shortcuts" in files
    1.55 +  prove_goal.el       	Emacs command to change proof format
    1.56 +  xlisten		shell script for running Isabelle under X
    1.57 +  teeinput		shell script to run Isabelle, logging inputs to a file
    1.58 +  Pure			directory of source files for Pure Isabelle
    1.59 +  Provers		directory of generic theorem provers
    1.60  
    1.61  xlisten sets up a window running Isabelle, with a separate small "listener"
    1.62  window, which keeps a log of all input lines.  This log is a useful record
    1.63 @@ -58,14 +61,16 @@
    1.64  least to record (if not to display) the log.
    1.65  
    1.66  The following subdirectories contain object-logics:
    1.67 -    FOL 	Natural deduction logic (intuitionistic and classical)
    1.68 -    ZF		Zermelo-Fraenkel Set theory
    1.69 -    CTT		Constructive Type Theory
    1.70 -    HOL		Classical Higher-Order Logic
    1.71 -    LK		Classical sequent calculus
    1.72 -    Modal	The modal logics T, S4, S43
    1.73 -    LCF         Logic for Computable Functions (domain theory)
    1.74 -    Cube	Barendregt's Lambda Cube
    1.75 +  FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    1.76 +  FOLP 	  First-Order Logic with Proof terms
    1.77 +  ZF	  Zermelo-Fraenkel set theory
    1.78 +  CTT	  Constructive Type Theory
    1.79 +  HOL	  Classical Higher-Order Logic
    1.80 +  LK	  Classical first-order sequent calculus
    1.81 +  Modal	  The modal logics T, S4, S43
    1.82 +  LCF     Logic for Computable Functions (domain theory)
    1.83 +  CCL	  Martin Coen's Classical Computational Logic
    1.84 +  Cube	  Barendregt's Lambda Cube
    1.85  
    1.86  Object-logics include examples files in subdirectory ex or file ex.ML.
    1.87  These files can be loaded in batch mode.  The commands can also be
    1.88 @@ -110,4 +115,4 @@
    1.89  D-8000 Muenchen 2
    1.90  Germany
    1.91  
    1.92 -Last updated 25 August 1992
    1.93 +Last updated 28 October 1993