1.1 --- a/src/LCF/Makefile	Tue Nov 09 16:09:34 1993 +0100
     1.2 +++ b/src/LCF/Makefile	Tue Nov 09 16:32:24 1993 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  BIN = $(ISABELLEBIN)
     1.6  COMP = $(ISABELLECOMP)
     1.7 -FILES =  ROOT.ML lcf.thy lcf.ML simpdata.ML pair.ML fix.ML ex.ML
     1.8 +FILES =  ROOT.ML lcf.thy lcf.ML simpdata.ML pair.ML fix.ML
     1.9  
    1.10  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.11  $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 

     2.1 --- a/src/LK/Makefile	Tue Nov 09 16:09:34 1993 +0100
     2.2 +++ b/src/LK/Makefile	Tue Nov 09 16:32:24 1993 +0100
     2.3 @@ -19,6 +19,7 @@
     2.4  BIN = $(ISABELLEBIN)
     2.5  COMP = $(ISABELLECOMP)
     2.6  FILES =  ROOT.ML lk.thy lk.ML
     2.7 +EX_FILES = ex/ROOT.ML ex/hardquant.ML ex/prop.ML ex/quant.ML
     2.8  
     2.9  $(BIN)/LK:   $(BIN)/Pure  $(FILES) 
    2.10  	case "$(COMP)" in \
    2.11 @@ -32,7 +33,7 @@
    2.12  $(BIN)/Pure:
    2.13  	cd ../Pure;  $(MAKE)
    2.14  
    2.15 -test:   ex/ROOT.ML  $(BIN)/LK
    2.16 +test:   ex/ROOT.ML  $(BIN)/LK  $(EX_FILES)
    2.17  	case "$(COMP)" in \
    2.18  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/LK ;;\
    2.19  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/LK;;\

     3.1 --- a/src/Modal/Makefile	Tue Nov 09 16:09:34 1993 +0100
     3.2 +++ b/src/Modal/Makefile	Tue Nov 09 16:32:24 1993 +0100
     3.3 @@ -19,6 +19,7 @@
     3.4  BIN = $(ISABELLEBIN)
     3.5  COMP = $(ISABELLECOMP)
     3.6  FILES = ROOT.ML modal0.thy prover.ML t.thy s4.thy s43.thy
     3.7 +EX_FILES = ex/ROOT.ML ex/S43thms.ML ex/S4thms.ML ex/Tthms.ML
     3.8  
     3.9  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    3.10  $(BIN)/Modal:   $(BIN)/LK  $(FILES) 
    3.11 @@ -32,7 +33,7 @@
    3.12  $(BIN)/LK:
    3.13  	cd ../LK;  $(MAKE)
    3.14  
    3.15 -test:   ex/ROOT.ML  $(BIN)/Modal
    3.16 +test:   ex/ROOT.ML  $(BIN)/Modal  $(EX_FILES)
    3.17  	case "$(COMP)" in \
    3.18  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/Modal ;;\
    3.19  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/Modal;;\

     4.1 --- a/src/ZF/Makefile	Tue Nov 09 16:09:34 1993 +0100
     4.2 +++ b/src/ZF/Makefile	Tue Nov 09 16:32:24 1993 +0100
     4.3 @@ -28,6 +28,16 @@
     4.4  	quniv.thy quniv.ML constructor.ML datatype.ML  \
     4.5  	fin.ML list.ML listfn.thy listfn.ML
     4.6  
     4.7 +EX_FILES = ex/ROOT.ML ex/acc.ML ex/bin.ML ex/binfn.ML ex/binfn.thy\
     4.8 +	   ex/bt.ML ex/bt_fn.ML ex/bt_fn.thy ex/comb.ML\
     4.9 +	   ex/contract0.ML ex/contract0.thy ex/counit.ML ex/data.ML\
    4.10 +	   ex/enum.ML ex/equiv.ML ex/equiv.thy ex/integ.ML ex/integ.thy\
    4.11 +	   ex/listn.ML ex/llist.ML ex/llist_eq.ML ex/llistfn.ML ex/llistfn.thy\
    4.12 +	   ex/misc.ML ex/parcontract.ML ex/primrec0.ML ex/primrec0.thy\
    4.13 +	   ex/prop.ML ex/proplog.ML ex/proplog.thy ex/ramsey.ML ex/ramsey.thy\
    4.14 +	   ex/rmap.ML ex/term.ML ex/termfn.ML ex/termfn.thy ex/tf.ML\
    4.15 +	   ex/tf_fn.ML ex/tf_fn.thy ex/twos_compl.ML
    4.16 +
    4.17  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    4.18  $(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
    4.19  	case "$(COMP)" in \
    4.20 @@ -40,7 +50,7 @@
    4.21  $(BIN)/FOL:
    4.22  	cd ../FOL;  $(MAKE)
    4.23  
    4.24 -test:   ex/ROOT.ML  $(BIN)/ZF
    4.25 +test:   ex/ROOT.ML  $(BIN)/ZF  $(EX_FILES)
    4.26  	case "$(COMP)" in \
    4.27  	poly*)	echo 'use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/ZF ;;\
    4.28  	sml*)	echo 'use"ex/ROOT.ML";' | $(BIN)/ZF;;\