--- a/src/CCL/Makefile Tue Nov 09 14:24:45 1993 +0100
+++ b/src/CCL/Makefile Tue Nov 09 16:09:34 1993 +0100
@@ -26,6 +26,9 @@
coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\
wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML
+EX_FILES = ex/ROOT.ML ex/flag.ML ex/flag.thy ex/list.ML ex/list.thy\
+ ex/nat.ML ex/nat.thy ex/stream.ML ex/stream.thy
+
#Uses cp rather than make_database because Poly/ML allows only 3 levels
$(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES)
case "$(COMP)" in \
@@ -38,7 +41,7 @@
$(BIN)/FOL:
cd ../FOL; $(MAKE)
-test: ex/ROOT.ML $(BIN)/CCL
+test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CCL;;\
--- a/src/CTT/Makefile Tue Nov 09 14:24:45 1993 +0100
+++ b/src/CTT/Makefile Tue Nov 09 16:09:34 1993 +0100
@@ -21,6 +21,8 @@
FILES = ROOT.ML ctt.thy ctt.ML bool.thy bool.ML \
arith.thy arith.ML rew.ML ../Provers/typedsimp.ML
+EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
+
$(BIN)/CTT: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/CTT"; quit();' \
@@ -33,7 +35,7 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/CTT
+test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\
--- a/src/Cube/Makefile Tue Nov 09 14:24:45 1993 +0100
+++ b/src/Cube/Makefile Tue Nov 09 16:09:34 1993 +0100
@@ -19,7 +19,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML cube.thy cube.ML ex.ML
+FILES = ROOT.ML cube.thy cube.ML
$(BIN)/Cube: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
--- a/src/FOL/Makefile Tue Nov 09 14:24:45 1993 +0100
+++ b/src/FOL/Makefile Tue Nov 09 16:09:34 1993 +0100
@@ -21,6 +21,11 @@
FILES = ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
+EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
+ ex/intro.ML ex/list.ML ex/list.thy ex/nat.ML ex/nat.thy\
+ ex/nat2.ML ex/nat2.thy ex/prolog.ML ex/prolog.thy ex/prop.ML\
+ ex/quant.ML
+
$(BIN)/FOL: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/FOL"; quit();' \
@@ -33,7 +38,7 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/FOL
+test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\
--- a/src/FOLP/Makefile Tue Nov 09 14:24:45 1993 +0100
+++ b/src/FOLP/Makefile Tue Nov 09 16:09:34 1993 +0100
@@ -21,6 +21,10 @@
FILES = ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
classical.ML ../Provers/simp.ML ../Provers/ind.ML
+EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
+ ex/intro.ML ex/nat.ML ex/nat.thy ex/prolog.ML ex/prolog.thy\
+ ex/prop.ML ex/quant.ML
+
$(BIN)/FOLP: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \
@@ -33,7 +37,7 @@
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/FOLP
+test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOLP;;\