# HG changeset patch
# User lcp
# Date 768820214 -7200
# Node ID e95e212512d18ed8f73222eda6c945e1cfea7d24
# Parent  5a7194eeb4ed281a24672596a06b0a4021ac449b
make-all-poly, make-all-nj: restored to main directory as examples
README: modified accordingly

diff -r 5a7194eeb4ed -r e95e212512d1 README
--- 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
diff -r 5a7194eeb4ed -r e95e212512d1 make-all-nj
--- /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 $*
diff -r 5a7194eeb4ed -r e95e212512d1 make-all-poly
--- /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 $*
diff -r 5a7194eeb4ed -r e95e212512d1 src/Tools/make-all-nj
--- /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 $*
diff -r 5a7194eeb4ed -r e95e212512d1 src/Tools/make-all-poly
--- /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 $*