1.1 --- a/src/CCL/Makefile Tue Nov 09 14:24:45 1993 +0100
1.2 +++ b/src/CCL/Makefile Tue Nov 09 16:09:34 1993 +0100
1.3 @@ -26,6 +26,9 @@
1.4 coinduction.ML hered.thy hered.ML trancl.thy trancl.ML\
1.5 wfd.thy wfd.ML genrec.ML typecheck.ML eval.ML fix.thy fix.ML
1.6
1.7 +EX_FILES = ex/ROOT.ML ex/flag.ML ex/flag.thy ex/list.ML ex/list.thy\
1.8 + ex/nat.ML ex/nat.thy ex/stream.ML ex/stream.thy
1.9 +
1.10 #Uses cp rather than make_database because Poly/ML allows only 3 levels
1.11 $(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES)
1.12 case "$(COMP)" in \
1.13 @@ -38,7 +41,7 @@
1.14 $(BIN)/FOL:
1.15 cd ../FOL; $(MAKE)
1.16
1.17 -test: ex/ROOT.ML $(BIN)/CCL
1.18 +test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
1.19 case "$(COMP)" in \
1.20 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\
1.21 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CCL;;\
2.1 --- a/src/CTT/Makefile Tue Nov 09 14:24:45 1993 +0100
2.2 +++ b/src/CTT/Makefile Tue Nov 09 16:09:34 1993 +0100
2.3 @@ -21,6 +21,8 @@
2.4 FILES = ROOT.ML ctt.thy ctt.ML bool.thy bool.ML \
2.5 arith.thy arith.ML rew.ML ../Provers/typedsimp.ML
2.6
2.7 +EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
2.8 +
2.9 $(BIN)/CTT: $(BIN)/Pure $(FILES)
2.10 case "$(COMP)" in \
2.11 poly*) echo 'make_database"$(BIN)/CTT"; quit();' \
2.12 @@ -33,7 +35,7 @@
2.13 $(BIN)/Pure:
2.14 cd ../Pure; $(MAKE)
2.15
2.16 -test: ex/ROOT.ML $(BIN)/CTT
2.17 +test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
2.18 case "$(COMP)" in \
2.19 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
2.20 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/CTT;;\
3.1 --- a/src/Cube/Makefile Tue Nov 09 14:24:45 1993 +0100
3.2 +++ b/src/Cube/Makefile Tue Nov 09 16:09:34 1993 +0100
3.3 @@ -19,7 +19,7 @@
3.4
3.5 BIN = $(ISABELLEBIN)
3.6 COMP = $(ISABELLECOMP)
3.7 -FILES = ROOT.ML cube.thy cube.ML ex.ML
3.8 +FILES = ROOT.ML cube.thy cube.ML
3.9
3.10 $(BIN)/Cube: $(BIN)/Pure $(FILES)
3.11 case "$(COMP)" in \
4.1 --- a/src/FOL/Makefile Tue Nov 09 14:24:45 1993 +0100
4.2 +++ b/src/FOL/Makefile Tue Nov 09 16:09:34 1993 +0100
4.3 @@ -21,6 +21,11 @@
4.4 FILES = ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
4.5 ../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
4.6
4.7 +EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
4.8 + ex/intro.ML ex/list.ML ex/list.thy ex/nat.ML ex/nat.thy\
4.9 + ex/nat2.ML ex/nat2.thy ex/prolog.ML ex/prolog.thy ex/prop.ML\
4.10 + ex/quant.ML
4.11 +
4.12 $(BIN)/FOL: $(BIN)/Pure $(FILES)
4.13 case "$(COMP)" in \
4.14 poly*) echo 'make_database"$(BIN)/FOL"; quit();' \
4.15 @@ -33,7 +38,7 @@
4.16 $(BIN)/Pure:
4.17 cd ../Pure; $(MAKE)
4.18
4.19 -test: ex/ROOT.ML $(BIN)/FOL
4.20 +test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
4.21 case "$(COMP)" in \
4.22 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
4.23 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOL;;\
5.1 --- a/src/FOLP/Makefile Tue Nov 09 14:24:45 1993 +0100
5.2 +++ b/src/FOLP/Makefile Tue Nov 09 16:09:34 1993 +0100
5.3 @@ -21,6 +21,10 @@
5.4 FILES = ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
5.5 classical.ML ../Provers/simp.ML ../Provers/ind.ML
5.6
5.7 +EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/if.ML ex/if.thy ex/int.ML\
5.8 + ex/intro.ML ex/nat.ML ex/nat.thy ex/prolog.ML ex/prolog.thy\
5.9 + ex/prop.ML ex/quant.ML
5.10 +
5.11 $(BIN)/FOLP: $(BIN)/Pure $(FILES)
5.12 case "$(COMP)" in \
5.13 poly*) echo 'make_database"$(BIN)/FOLP"; quit();' \
5.14 @@ -33,7 +37,7 @@
5.15 $(BIN)/Pure:
5.16 cd ../Pure; $(MAKE)
5.17
5.18 -test: ex/ROOT.ML $(BIN)/FOLP
5.19 +test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
5.20 case "$(COMP)" in \
5.21 poly*) echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
5.22 sml*) echo 'use"ex/ROOT.ML";' | $(BIN)/FOLP;;\