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

diff -r d4730dd72226 -r e04cb6295a3f src/LCF/Makefile
--- 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) 
diff -r d4730dd72226 -r e04cb6295a3f src/LK/Makefile
--- 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;;\
diff -r d4730dd72226 -r e04cb6295a3f src/Modal/Makefile
--- 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;;\
diff -r d4730dd72226 -r e04cb6295a3f src/ZF/Makefile
--- 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;;\