make-all-poly, make-all-nj: restored to main directory as examples
README: modified accordingly
--- a/README Wed May 11 12:29:34 1994 +0200
+++ b/README Fri May 13 11:10:14 1994 +0200
@@ -20,8 +20,9 @@
free and its code sometimes runs faster. Both compilers are perfectly
satisfactory for running Isabelle.
-The Makefiles and make-all use enviroment variables that you should set
-according to your site configuration.
+The Makefiles and make-all use environment variables that you should set
+according to your site configuration. See file 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. When using Poly/ML, ISABELLEBIN must be an absolute pathname (one
@@ -48,6 +49,8 @@
Other important files include...
COPYRIGHT Copyright notice and Disclaimer of Warranty
make-all shell script for building entire system
+ make-all-poly sample make-all invocation for Poly/ML
+ make-all-nj sample make-all invocation for SML of NJ
change_simp shell script to help convert sources to new simplifier
expandshort shell script to expand "shortcuts" in files
prove_goal.el Emacs command to change proof format
@@ -65,11 +68,12 @@
FOL Natural deduction First-Order Logic (intuitionistic and classical)
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
- HOL Classical Higher-Order Logic
LK Classical first-order sequent calculus
Modal The modal logics T, S4, S43
- LCF Logic for Computable Functions (domain theory)
CCL Martin Coen's Classical Computational Logic
Cube Barendregt's Lambda Cube
@@ -121,4 +125,4 @@
D-80290 Muenchen
Germany
-Last updated 13 December 1993
+Last updated 13 May 1994
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/make-all-nj Fri May 13 11:10:14 1994 +0200
@@ -0,0 +1,8 @@
+#! /bin/sh
+#Make entire system using Standard ML of New Jersey
+#Pathnames will have to be modified for your site
+ISABELLEBIN=/homes/`whoami`/bin
+ISABELLECOMP=sml
+ISABELLEMAKE=Makefile.NJ
+export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+nohup make-all $*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/make-all-poly Fri May 13 11:10:14 1994 +0200
@@ -0,0 +1,9 @@
+#! /bin/sh
+#Make entire system using Poly/ML
+#Pathnames will have to be modified for your site
+ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
+ISABELLEBIN=/homes/`whoami`/bin
+ISABELLECOMP="poly -noDisplay -h 15000"
+ISABELLEMAKE=Makefile
+export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+nohup make-all $*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/make-all-nj Fri May 13 11:10:14 1994 +0200
@@ -0,0 +1,8 @@
+#! /bin/sh
+#Make entire system using Standard ML of New Jersey
+#Pathnames will have to be modified for your site
+ISABELLEBIN=/homes/`whoami`/bin
+ISABELLECOMP=sml
+ISABELLEMAKE=Makefile.NJ
+export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+nohup make-all $*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/make-all-poly Fri May 13 11:10:14 1994 +0200
@@ -0,0 +1,9 @@
+#! /bin/sh
+#Make entire system using Poly/ML
+#Pathnames will have to be modified for your site
+ML_DBASE=/usr/groups/theory/poly/`arch`/ML_dbase
+ISABELLEBIN=/homes/`whoami`/bin
+ISABELLECOMP="poly -noDisplay -h 15000"
+ISABELLEMAKE=Makefile
+export ML_DBASE ISABELLEBIN ISABELLECOMP ISABELLEMAKE
+nohup make-all $*