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
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/make-all-nj Fri May 13 11:10:14 1994 +0200
2.3 @@ -0,0 +1,8 @@
2.4 +#! /bin/sh
2.5 +#Make entire system using Standard ML of New Jersey
2.6 +#Pathnames will have to be modified for your site
2.7 +ISABELLEBIN=/homes/`whoami`/bin
2.8 +ISABELLECOMP=sml
2.9 +ISABELLEMAKE=Makefile.NJ
2.10 +export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
2.11 +nohup make-all $*
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/make-all-poly Fri May 13 11:10:14 1994 +0200
3.3 @@ -0,0 +1,9 @@
3.4 +#! /bin/sh
3.5 +#Make entire system using Poly/ML
3.6 +#Pathnames will have to be modified for your site
3.7 +ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
3.8 +ISABELLEBIN=/homes/`whoami`/bin
3.9 +ISABELLECOMP="poly -noDisplay -h 15000"
3.10 +ISABELLEMAKE=Makefile
3.11 +export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
3.12 +nohup make-all $*
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/make-all-nj Fri May 13 11:10:14 1994 +0200
4.3 @@ -0,0 +1,8 @@
4.4 +#! /bin/sh
4.5 +#Make entire system using Standard ML of New Jersey
4.6 +#Pathnames will have to be modified for your site
4.7 +ISABELLEBIN=/homes/`whoami`/bin
4.8 +ISABELLECOMP=sml
4.9 +ISABELLEMAKE=Makefile.NJ
4.10 +export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
4.11 +nohup make-all $*
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/make-all-poly Fri May 13 11:10:14 1994 +0200
5.3 @@ -0,0 +1,9 @@
5.4 +#! /bin/sh
5.5 +#Make entire system using Poly/ML
5.6 +#Pathnames will have to be modified for your site
5.7 +ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
5.8 +ISABELLEBIN=/homes/`whoami`/bin
5.9 +ISABELLECOMP="poly -noDisplay -h 15000"
5.10 +ISABELLEMAKE=Makefile
5.11 +export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
5.12 +nohup make-all $*