README
changeset 370 e95e212512d1
parent 196 7646f5b4653c
child 470 6cb6dd05d761
     1.1 --- a/README	Wed May 11 12:29:34 1994 +0200
     1.2 +++ b/README	Fri May 13 11:10:14 1994 +0200
     1.3 @@ -20,8 +20,9 @@
     1.4  free and its code sometimes runs faster.  Both compilers are perfectly
     1.5  satisfactory for running Isabelle.
     1.6  
     1.7 -The Makefiles and make-all use enviroment variables that you should set
     1.8 -according to your site configuration.
     1.9 +The Makefiles and make-all use environment variables that you should set
    1.10 +according to your site configuration.  See file make-all-nj for an example
    1.11 +using the Bourne shell, sh.
    1.12  
    1.13  ISABELLEBIN is the directory to hold Poly/ML databases or New Jersey ML
    1.14  images.  When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
    1.15 @@ -48,6 +49,8 @@
    1.16  Other important files include...
    1.17    COPYRIGHT   		Copyright notice and Disclaimer of Warranty
    1.18    make-all		shell script for building entire system
    1.19 +  make-all-poly		sample make-all invocation for Poly/ML
    1.20 +  make-all-nj		sample make-all invocation for SML of NJ
    1.21    change_simp		shell script to help convert sources to new simplifier
    1.22    expandshort		shell script to expand "shortcuts" in files
    1.23    prove_goal.el       	Emacs command to change proof format
    1.24 @@ -65,11 +68,12 @@
    1.25    FOL 	  Natural deduction First-Order Logic (intuitionistic and classical)
    1.26    FOLP 	  First-Order Logic with Proof terms
    1.27    ZF	  Zermelo-Fraenkel set theory
    1.28 +  HOL	  Classical Higher-Order Logic
    1.29 +  LCF     Logic for Computable Functions (domain theory) built upon FOL
    1.30 +  HOLCF   A version of LCF built upon HOL
    1.31    CTT	  Constructive Type Theory
    1.32 -  HOL	  Classical Higher-Order Logic
    1.33    LK	  Classical first-order sequent calculus
    1.34    Modal	  The modal logics T, S4, S43
    1.35 -  LCF     Logic for Computable Functions (domain theory)
    1.36    CCL	  Martin Coen's Classical Computational Logic
    1.37    Cube	  Barendregt's Lambda Cube
    1.38  
    1.39 @@ -121,4 +125,4 @@
    1.40  D-80290 Muenchen
    1.41  Germany
    1.42  
    1.43 -Last updated 13 December 1993
    1.44 +Last updated 13 May 1994