log files;
authorwenzelm
Fri Dec 19 10:18:58 1997 +0100 (1997-12-19)
changeset 4447b7ee449eb345
parent 4446 097004a470fb
child 4448 b587d40ad474
log files;
'clean' target;
src/CCL/IsaMakefile
src/CTT/IsaMakefile
src/Cube/IsaMakefile
src/FOL/IsaMakefile
src/FOLP/IsaMakefile
src/HOL/IsaMakefile
src/HOLCF/IsaMakefile
src/LCF/IsaMakefile
src/Sequents/IsaMakefile
src/ZF/IsaMakefile
     1.1 --- a/src/CCL/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     1.2 +++ b/src/CCL/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     1.3 @@ -5,6 +5,7 @@
     1.4  #
     1.5  
     1.6  OUT = $(ISABELLE_OUTPUT)
     1.7 +LOG = $(OUT)/log
     1.8  
     1.9  SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
    1.10  	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
    1.11 @@ -23,7 +24,13 @@
    1.12  $(OUT)/FOL:
    1.13  	@cd ../FOL; $(ISATOOL) make
    1.14  
    1.15 -test: ex/ROOT.ML $(OUT)/CCL $(EX_FILES)
    1.16 +$(LOG)/CCL-ex.gz: ex/ROOT.ML $(OUT)/CCL $(EX_FILES)
    1.17  	@$(ISATOOL) usedir $(OUT)/CCL ex
    1.18  
    1.19 +test: $(OUT)/CCL $(LOG)/CCL-ex.gz
    1.20 +
    1.21 +clean:
    1.22 +	@rm -f $(OUT)/CCL $(LOG)/CCL-ex.gz
    1.23 +
    1.24 +
    1.25  .PRECIOUS: $(OUT)/FOL $(OUT)/CCL
     2.1 --- a/src/CTT/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     2.2 +++ b/src/CTT/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     2.3 @@ -5,6 +5,7 @@
     2.4  #
     2.5  
     2.6  OUT = $(ISABELLE_OUTPUT)
     2.7 +LOG = $(OUT)/log
     2.8  
     2.9  FILES =	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
    2.10  	Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
    2.11 @@ -17,7 +18,13 @@
    2.12  $(OUT)/Pure:
    2.13  	@cd ../Pure; $(ISATOOL) make
    2.14  
    2.15 -test: ex/ROOT.ML $(OUT)/CTT $(EX_FILES)
    2.16 +$(LOG)/CTT-ex.gz: ex/ROOT.ML $(OUT)/CTT $(EX_FILES)
    2.17  	@$(ISATOOL) usedir $(OUT)/CTT ex
    2.18  
    2.19 +test: $(OUT)/CTT $(LOG)/CTT-ex.gz
    2.20 +
    2.21 +clean:
    2.22 +	@rm -f $(OUT)/CTT $(LOG)/CTT-ex.gz
    2.23 +
    2.24 +
    2.25  .PRECIOUS: $(OUT)/Pure $(OUT)/CTT
     3.1 --- a/src/Cube/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     3.2 +++ b/src/Cube/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     3.3 @@ -5,6 +5,8 @@
     3.4  #
     3.5  
     3.6  OUT = $(ISABELLE_OUTPUT)
     3.7 +LOG = $(OUT)/log
     3.8 +
     3.9  FILES =	ROOT.ML Cube.thy Cube.ML
    3.10  
    3.11  $(OUT)/Cube: $(OUT)/Pure $(FILES)
    3.12 @@ -13,7 +15,13 @@
    3.13  $(OUT)/Pure:
    3.14  	@cd ../Pure; $(ISATOOL) make
    3.15  
    3.16 -test: ex/ROOT.ML ex/ex.ML $(OUT)/Cube
    3.17 +$(LOG)/Cube-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/Cube
    3.18  	@$(ISATOOL) usedir $(OUT)/Cube ex
    3.19  
    3.20 +test: $(OUT)/Cube $(LOG)/Cube-ex.gz
    3.21 +
    3.22 +clean:
    3.23 +	@rm -f $(OUT)/Cube $(LOG)/Cube-ex.gz
    3.24 +
    3.25 +
    3.26  .PRECIOUS: $(OUT)/Pure $(OUT)/Cube
     4.1 --- a/src/FOL/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     4.2 +++ b/src/FOL/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     4.3 @@ -5,12 +5,13 @@
     4.4  #
     4.5  
     4.6  OUT = $(ISABELLE_OUTPUT)
     4.7 +LOG = $(OUT)/log
     4.8  
     4.9  PROVERS = hypsubst.ML classical.ML blast.ML \
    4.10  	simplifier.ML splitter.ML ind.ML 
    4.11  
    4.12  FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    4.13 -	fologic.ML cladata.ML $(PROVERS:%=../Provers/%)
    4.14 +	fologic.ML cladata.ML $(PROVERS:%=$(ISABELLE_HOME)/src/Provers/%)
    4.15  
    4.16  EX_NAMES = If List Nat Nat2 Prolog IffOracle
    4.17  EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
    4.18 @@ -23,7 +24,13 @@
    4.19  $(OUT)/Pure:
    4.20  	@cd ../Pure; $(ISATOOL) make
    4.21  
    4.22 -test: ex/ROOT.ML $(OUT)/FOL $(EX_FILES)
    4.23 +$(LOG)/FOL-ex.gz: ex/ROOT.ML $(OUT)/FOL $(EX_FILES)
    4.24  	@$(ISATOOL) usedir $(OUT)/FOL ex
    4.25  
    4.26 +test: $(OUT)/FOL $(LOG)/FOL-ex.gz
    4.27 +
    4.28 +clean:
    4.29 +	@rm -f $(OUT)/FOL $(LOG)/FOL-ex.gz
    4.30 +
    4.31 +
    4.32  .PRECIOUS: $(OUT)/Pure $(OUT)/FOL
     5.1 --- a/src/FOLP/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     5.2 +++ b/src/FOLP/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     5.3 @@ -5,6 +5,7 @@
     5.4  #
     5.5  
     5.6  OUT = $(ISABELLE_OUTPUT)
     5.7 +LOG = $(OUT)/log
     5.8  
     5.9  FILES =	ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML \
    5.10  	hypsubst.ML classical.ML simp.ML
    5.11 @@ -19,7 +20,13 @@
    5.12  $(OUT)/Pure:
    5.13  	@cd ../Pure; $(ISATOOL) make
    5.14  
    5.15 -test: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES)
    5.16 +$(LOG)/FOLP-ex.gz: ex/ROOT.ML $(OUT)/FOLP $(EX_FILES)
    5.17  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    5.18  
    5.19 +test: $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    5.20 +
    5.21 +clean:
    5.22 +	@rm -f $(OUT)/FOLP $(LOG)/FOLP-ex.gz
    5.23 +
    5.24 +
    5.25  .PRECIOUS: $(OUT)/Pure $(OUT)/FOLP
     6.1 --- a/src/HOL/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     6.2 +++ b/src/HOL/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     6.3 @@ -7,6 +7,7 @@
     6.4  #### Base system
     6.5  
     6.6  OUT = $(ISABELLE_OUTPUT)
     6.7 +LOG = $(OUT)/log
     6.8  
     6.9  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
    6.10  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
    6.11 @@ -41,7 +42,7 @@
    6.12  INDUCT_FILES = Induct/ROOT.ML \
    6.13  	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
    6.14  
    6.15 -Induct:	$(OUT)/HOL $(INDUCT_FILES)
    6.16 +$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
    6.17  	@$(ISATOOL) usedir $(OUT)/HOL Induct
    6.18  
    6.19  
    6.20 @@ -50,7 +51,7 @@
    6.21  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    6.22  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    6.23  
    6.24 -IMP:	$(OUT)/HOL $(IMP_FILES)
    6.25 +$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
    6.26  	@$(ISATOOL) usedir $(OUT)/HOL IMP
    6.27  
    6.28  
    6.29 @@ -60,7 +61,7 @@
    6.30  Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
    6.31  	      $(Hoare_NAMES:%=Hoare/%.ML)
    6.32  
    6.33 -Hoare:	$(OUT)/HOL $(Hoare_FILES)
    6.34 +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
    6.35  	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    6.36  
    6.37  
    6.38 @@ -71,7 +72,7 @@
    6.39  INTEG_FILES = Integ/ROOT.ML \
    6.40  	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    6.41  
    6.42 -Integ:	$(OUT)/HOL $(INTEG_FILES)
    6.43 +$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
    6.44  	@$(ISATOOL) usedir $(OUT)/HOL Integ
    6.45  
    6.46  
    6.47 @@ -97,16 +98,16 @@
    6.48  	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
    6.49  
    6.50  
    6.51 -TLA: $(OUT)/HOL $(TLA_FILES)
    6.52 +$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
    6.53  	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
    6.54  
    6.55 -TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES)
    6.56 +$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
    6.57  	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
    6.58  
    6.59 -TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES)
    6.60 +$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
    6.61  	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
    6.62  
    6.63 -TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES)
    6.64 +$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
    6.65  	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
    6.66  
    6.67  
    6.68 @@ -115,7 +116,7 @@
    6.69  IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
    6.70    IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
    6.71  
    6.72 -IOA: $(OUT)/HOL $(IOA_FILES)
    6.73 +$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
    6.74  	@$(ISATOOL) usedir $(OUT)/HOL IOA
    6.75  
    6.76  
    6.77 @@ -128,7 +129,7 @@
    6.78  
    6.79  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    6.80  
    6.81 -Auth:	$(OUT)/HOL $(AUTH_FILES)
    6.82 +$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
    6.83  	@$(ISATOOL) usedir $(OUT)/HOL Auth
    6.84  
    6.85  
    6.86 @@ -138,7 +139,7 @@
    6.87    Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
    6.88    Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
    6.89  
    6.90 -Modelcheck: $(OUT)/HOL $(MC_FILES)
    6.91 +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
    6.92  	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
    6.93  
    6.94  
    6.95 @@ -149,7 +150,7 @@
    6.96  SUBST_FILES = Subst/ROOT.ML \
    6.97  	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    6.98  
    6.99 -Subst:	$(OUT)/HOL $(SUBST_FILES)
   6.100 +$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
   6.101  	@$(ISATOOL) usedir $(OUT)/HOL Subst
   6.102  
   6.103  
   6.104 @@ -160,7 +161,7 @@
   6.105  LAMBDA_FILES = Lambda/ROOT.ML \
   6.106  	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   6.107  
   6.108 -Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
   6.109 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
   6.110  	@$(ISATOOL) usedir $(OUT)/HOL Lambda
   6.111  
   6.112  
   6.113 @@ -171,7 +172,7 @@
   6.114  W0_FILES = W0/ROOT.ML \
   6.115  	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
   6.116  
   6.117 -W0: $(OUT)/HOL $(W0_FILES)
   6.118 +$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
   6.119  	@$(ISATOOL) usedir $(OUT)/HOL W0
   6.120  
   6.121  
   6.122 @@ -182,7 +183,7 @@
   6.123  MINIML_FILES = MiniML/ROOT.ML \
   6.124  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   6.125  
   6.126 -MiniML: $(OUT)/HOL $(MINIML_FILES)
   6.127 +$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
   6.128  	@$(ISATOOL) usedir $(OUT)/HOL MiniML
   6.129  
   6.130  
   6.131 @@ -193,7 +194,7 @@
   6.132  LEX_FILES = Lex/ROOT.ML \
   6.133  	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   6.134  
   6.135 -Lex:	$(OUT)/HOL $(LEX_FILES)
   6.136 +$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
   6.137  	@$(ISATOOL) usedir $(OUT)/HOL Lex
   6.138  
   6.139  
   6.140 @@ -212,15 +213,19 @@
   6.141  	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
   6.142  	Xor.ML Xor.thy
   6.143  
   6.144 -AXCLASSES_FILES = AxClasses/ROOT.ML \
   6.145 -	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
   6.146 -	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
   6.147 -	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   6.148 +$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
   6.149 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   6.150 +
   6.151 +$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
   6.152 +  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
   6.153 +	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   6.154  
   6.155 -AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
   6.156 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   6.157 -	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
   6.158 +$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
   6.159 +  $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
   6.160  	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
   6.161 +
   6.162 +$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
   6.163 +  $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   6.164  	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
   6.165  
   6.166  
   6.167 @@ -229,7 +234,8 @@
   6.168  QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
   6.169  	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
   6.170  	Quot/FRACT.thy Quot/FRACT.ML
   6.171 -Quot:	$(OUT)/HOL $(QUOT_FILES)
   6.172 +
   6.173 +$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
   6.174  	@$(ISATOOL) usedir $(OUT)/HOL Quot
   6.175  
   6.176  
   6.177 @@ -240,16 +246,25 @@
   6.178  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   6.179  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   6.180  
   6.181 -ex:	$(OUT)/HOL $(EX_FILES)
   6.182 +$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
   6.183  	@$(ISATOOL) usedir $(OUT)/HOL ex
   6.184  
   6.185  
   6.186  ## Full test
   6.187  
   6.188 -test:	$(OUT)/HOL \
   6.189 -	  Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
   6.190 -	  W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
   6.191 -	echo 'Test examples ran successfully' > test
   6.192 +ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
   6.193 +  $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
   6.194 +  $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
   6.195 +  $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
   6.196 +  $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
   6.197 +  $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
   6.198 +  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
   6.199 +  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
   6.200 +
   6.201 +test: $(ALL_TARGETS)
   6.202 +
   6.203 +clean:
   6.204 +	@rm -f $(ALL_TARGETS)
   6.205  
   6.206  
   6.207  .PRECIOUS: $(OUT)/Pure $(OUT)/HOL
     7.1 --- a/src/HOLCF/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     7.2 +++ b/src/HOLCF/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     7.3 @@ -7,6 +7,7 @@
     7.4  #### Base system
     7.5  
     7.6  OUT = $(ISABELLE_OUTPUT)
     7.7 +LOG = $(OUT)/log
     7.8  
     7.9  THYS = Porder.thy Porder0.thy Pcpo.thy \
    7.10         Fun1.thy Fun2.thy Fun3.thy \
    7.11 @@ -79,13 +80,13 @@
    7.12    IOA/NTP/Spec.thy 
    7.13  
    7.14   
    7.15 -IOA: $(OUT)/HOLCF $(IOA_FILES)
    7.16 +$(OUT)/IOA: $(OUT)/HOLCF $(IOA_FILES)
    7.17  	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
    7.18  
    7.19 -IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
    7.20 +$(LOG)/IOA-ABP.gz: $(OUT)/IOA $(IOA_ABP_FILES)
    7.21  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
    7.22  
    7.23 -IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
    7.24 +$(LOG)/IOA-NTP.gz: $(OUT)/IOA $(IOA_NTP_FILES)
    7.25  	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
    7.26  
    7.27  
    7.28 @@ -94,7 +95,7 @@
    7.29  IMP_THYS = IMP/Denotational.thy
    7.30  IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    7.31  
    7.32 -IMP:	$(OUT)/HOLCF $(IMP_FILES)
    7.33 +$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF $(IMP_FILES)
    7.34  	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    7.35  
    7.36  
    7.37 @@ -106,14 +107,19 @@
    7.38  
    7.39  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    7.40  
    7.41 -ex:	ex/ROOT.ML $(EX_FILES)
    7.42 +$(LOG)/HOLCF-ex.gz: ex/ROOT.ML $(EX_FILES)
    7.43  	@$(ISATOOL) usedir $(OUT)/HOLCF ex
    7.44  
    7.45  
    7.46  ## Full test
    7.47  
    7.48 -test:	$(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP ex
    7.49 -	echo 'Test examples ran successfully' > test
    7.50 +ALL_TARGETS = $(OUT)/HOLCF $(OUT)/IOA $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
    7.51 +  $(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz
    7.52 +
    7.53 +test: $(ALL_TARGETS)
    7.54 +
    7.55 +clean:
    7.56 +	@rm -f $(ALL_TARGETS)
    7.57  
    7.58  
    7.59  .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
     8.1 --- a/src/LCF/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     8.2 +++ b/src/LCF/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     8.3 @@ -5,6 +5,8 @@
     8.4  #
     8.5  
     8.6  OUT = $(ISABELLE_OUTPUT)
     8.7 +LOG = $(OUT)/log
     8.8 +
     8.9  FILES =	ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    8.10  
    8.11  $(OUT)/LCF: $(OUT)/FOL $(FILES)
    8.12 @@ -13,7 +15,13 @@
    8.13  $(OUT)/FOL:
    8.14  	@cd ../FOL; $(ISATOOL) make
    8.15  
    8.16 -test: ex/ROOT.ML ex/ex.ML $(OUT)/LCF
    8.17 +$(LOG)/LCF-ex.gz: ex/ROOT.ML ex/ex.ML $(OUT)/LCF
    8.18  	@$(ISATOOL) usedir $(OUT)/LCF ex
    8.19  
    8.20 +test: $(OUT)/LCF $(LOG)/LCF-ex.gz
    8.21 +
    8.22 +clean:
    8.23 +	@rm -f $(OUT)/LCF $(LOG)/LCF-ex.gz
    8.24 +
    8.25 +
    8.26  .PRECIOUS: $(OUT)/FOL $(OUT)/LCF
     9.1 --- a/src/Sequents/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
     9.2 +++ b/src/Sequents/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
     9.3 @@ -5,6 +5,7 @@
     9.4  #
     9.5  
     9.6  OUT = $(ISABELLE_OUTPUT)
     9.7 +LOG = $(OUT)/log
     9.8  
     9.9  NAMES = ILL LK S4 S43 T
    9.10  FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
    9.11 @@ -22,7 +23,13 @@
    9.12  $(OUT)/Pure:
    9.13  	@cd ../Pure; $(ISATOOL) make
    9.14  
    9.15 -test: $(OUT)/Sequents $(EX_FILES)
    9.16 +$(LOG)/Sequents-ex.gz: $(OUT)/Sequents $(EX_FILES)
    9.17  	@$(ISATOOL) usedir $(OUT)/Sequents ex
    9.18  
    9.19 +test: $(OUT)/Sequents $(LOG)/Sequents-ex.gz
    9.20 +
    9.21 +clean:
    9.22 +	@rm -f $(OUT)/Sequents $(LOG)/Sequents-ex.gz
    9.23 +
    9.24 +
    9.25  .PRECIOUS: $(OUT)/Pure $(OUT)/Sequents
    10.1 --- a/src/ZF/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
    10.2 +++ b/src/ZF/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
    10.3 @@ -7,6 +7,7 @@
    10.4  #### Base system
    10.5  
    10.6  OUT = $(ISABELLE_OUTPUT)
    10.7 +LOG = $(OUT)/log
    10.8  
    10.9  NAMES = ZF upair subset pair domrange \
   10.10  	func AC equalities Bool \
   10.11 @@ -35,7 +36,7 @@
   10.12  IMP_NAMES = Com Denotation Equiv
   10.13  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
   10.14  
   10.15 -IMP: $(OUT)/ZF $(IMP_FILES)
   10.16 +$(LOG)/ZF-IMP.gz: $(OUT)/ZF $(IMP_FILES)
   10.17  	@$(ISATOOL) usedir $(OUT)/ZF IMP
   10.18  
   10.19  
   10.20 @@ -46,7 +47,7 @@
   10.21  COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy \
   10.22  	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
   10.23  
   10.24 -Coind: $(OUT)/ZF $(COIND_FILES)
   10.25 +$(LOG)/ZF-Coind.gz: $(OUT)/ZF $(COIND_FILES)
   10.26  	@$(ISATOOL) usedir $(OUT)/ZF Coind
   10.27  
   10.28  
   10.29 @@ -62,7 +63,7 @@
   10.30  	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
   10.31  	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
   10.32  
   10.33 -AC: $(OUT)/ZF $(AC_FILES)
   10.34 +$(LOG)/ZF-AC.gz: $(OUT)/ZF $(AC_FILES)
   10.35  	@$(ISATOOL) usedir $(OUT)/ZF AC
   10.36  
   10.37  
   10.38 @@ -73,7 +74,7 @@
   10.39  
   10.40  RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
   10.41  
   10.42 -Resid: $(OUT)/ZF $(RESID_FILES)
   10.43 +$(LOG)/ZF-Resid.gz: $(OUT)/ZF $(RESID_FILES)
   10.44  	@$(ISATOOL) usedir $(OUT)/ZF Resid
   10.45  
   10.46  
   10.47 @@ -84,13 +85,19 @@
   10.48  
   10.49  EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   10.50  
   10.51 -ex: $(OUT)/ZF $(EX_FILES)
   10.52 +$(LOG)/ZF-ex.gz: $(OUT)/ZF $(EX_FILES)
   10.53  	@$(ISATOOL) usedir $(OUT)/ZF ex
   10.54  
   10.55  
   10.56  ## Full test
   10.57  
   10.58 -test: $(OUT)/ZF IMP Coind AC Resid ex
   10.59 -	echo 'Test examples ran successfully' > test
   10.60 +ALL_TARGETS = $(OUT)/ZF $(LOG)/ZF-IMP.gz $(LOG)/ZF-Coind.gz \
   10.61 +  $(LOG)/ZF-AC.gz $(LOG)/ZF-Resid.gz $(LOG)/ZF-ex.gz
   10.62 +
   10.63 +test: $(ALL_TARGETS)
   10.64 +
   10.65 +clean:
   10.66 +	@rm -f $(ALL_TARGETS)
   10.67 +
   10.68  
   10.69  .PRECIOUS: $(OUT)/FOL $(OUT)/ZF