--- a/src/LCF/Makefile Tue Nov 09 16:09:34 1993 +0100
+++ b/src/LCF/Makefile Tue Nov 09 16:32:24 1993 +0100
@@ -18,7 +18,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML lcf.thy lcf.ML simpdata.ML pair.ML fix.ML ex.ML
+FILES = ROOT.ML lcf.thy lcf.ML simpdata.ML pair.ML fix.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/LCF: $(BIN)/FOL $(FILES)
--- a/src/LK/Makefile Tue Nov 09 16:09:34 1993 +0100
+++ b/src/LK/Makefile Tue Nov 09 16:32:24 1993 +0100
@@ -19,6 +19,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
FILES = ROOT.ML lk.thy lk.ML
+EX_FILES = ex/ROOT.ML ex/hardquant.ML ex/prop.ML ex/quant.ML
$(BIN)/LK: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
@@ -32,7 +33,7 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/LK
+test: ex/ROOT.ML $(BIN)/LK $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/LK ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/LK;;\
--- a/src/Modal/Makefile Tue Nov 09 16:09:34 1993 +0100
+++ b/src/Modal/Makefile Tue Nov 09 16:32:24 1993 +0100
@@ -19,6 +19,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
FILES = ROOT.ML modal0.thy prover.ML t.thy s4.thy s43.thy
+EX_FILES = ex/ROOT.ML ex/S43thms.ML ex/S4thms.ML ex/Tthms.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/Modal: $(BIN)/LK $(FILES)
@@ -32,7 +33,7 @@
$(BIN)/LK:
cd ../LK; $(MAKE)
-test: ex/ROOT.ML $(BIN)/Modal
+test: ex/ROOT.ML $(BIN)/Modal $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/Modal ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/Modal;;\
--- a/src/ZF/Makefile Tue Nov 09 16:09:34 1993 +0100
+++ b/src/ZF/Makefile Tue Nov 09 16:32:24 1993 +0100
@@ -28,6 +28,16 @@
quniv.thy quniv.ML constructor.ML datatype.ML \
fin.ML list.ML listfn.thy listfn.ML
+EX_FILES = ex/ROOT.ML ex/acc.ML ex/bin.ML ex/binfn.ML ex/binfn.thy\
+ ex/bt.ML ex/bt_fn.ML ex/bt_fn.thy ex/comb.ML\
+ ex/contract0.ML ex/contract0.thy ex/counit.ML ex/data.ML\
+ ex/enum.ML ex/equiv.ML ex/equiv.thy ex/integ.ML ex/integ.thy\
+ ex/listn.ML ex/llist.ML ex/llist_eq.ML ex/llistfn.ML ex/llistfn.thy\
+ ex/misc.ML ex/parcontract.ML ex/primrec0.ML ex/primrec0.thy\
+ ex/prop.ML ex/proplog.ML ex/proplog.thy ex/ramsey.ML ex/ramsey.thy\
+ ex/rmap.ML ex/term.ML ex/termfn.ML ex/termfn.thy ex/tf.ML\
+ ex/tf_fn.ML ex/tf_fn.thy ex/twos_compl.ML
+
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/ZF: $(BIN)/FOL $(FILES)
case "$(COMP)" in \
@@ -40,7 +50,7 @@
$(BIN)/FOL:
cd ../FOL; $(MAKE)
-test: ex/ROOT.ML $(BIN)/ZF
+test: ex/ROOT.ML $(BIN)/ZF $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\