# HG changeset patch
# User lcp
# Date 752857774 -3600
# Node ID d4730dd72226c87ab5095f5c72567b6bbf968ddc
# Parent  e95b98536b3df78e83b550607e2ad3f4b5cc92b0
Target "test" now depends on examples files

diff -r e95b98536b3d -r d4730dd72226 src/CCL/Makefile
--- 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;;\
diff -r e95b98536b3d -r d4730dd72226 src/CTT/Makefile
--- 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;;\
diff -r e95b98536b3d -r d4730dd72226 src/Cube/Makefile
--- 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 \
diff -r e95b98536b3d -r d4730dd72226 src/FOL/Makefile
--- 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;;\
diff -r e95b98536b3d -r d4730dd72226 src/FOLP/Makefile
--- 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;;\