diff -r 097004a470fb -r b7ee449eb345 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Dec 19 10:18:03 1997 +0100
+++ b/src/HOL/IsaMakefile	Fri Dec 19 10:18:58 1997 +0100
@@ -7,6 +7,7 @@
 #### Base system
 
 OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
@@ -41,7 +42,7 @@
 INDUCT_FILES = Induct/ROOT.ML \
 	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
 
-Induct:	$(OUT)/HOL $(INDUCT_FILES)
+$(LOG)/HOL-Induct.gz: $(OUT)/HOL $(INDUCT_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Induct
 
 
@@ -50,7 +51,7 @@
 IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
-IMP:	$(OUT)/HOL $(IMP_FILES)
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL $(IMP_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL IMP
 
 
@@ -60,7 +61,7 @@
 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
 	      $(Hoare_NAMES:%=Hoare/%.ML)
 
-Hoare:	$(OUT)/HOL $(Hoare_FILES)
+$(LOG)/HOL-Hoare.gz: $(OUT)/HOL $(Hoare_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Hoare
 
 
@@ -71,7 +72,7 @@
 INTEG_FILES = Integ/ROOT.ML \
 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
-Integ:	$(OUT)/HOL $(INTEG_FILES)
+$(LOG)/HOL-Integ.gz: $(OUT)/HOL $(INTEG_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Integ
 
 
@@ -97,16 +98,16 @@
 	TLA/Memory/RPCParameters.ML TLA/Memory/RPCParameters.thy
 
 
-TLA: $(OUT)/HOL $(TLA_FILES)
+$(OUT)/TLA: $(OUT)/HOL $(TLA_FILES)
 	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
 
-TLA_Inc: $(OUT)/TLA $(TLA_INC_FILES)
+$(LOG)/TLA-Inc.gz: $(OUT)/TLA $(TLA_INC_FILES)
 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
 
-TLA_Buffer: $(OUT)/TLA $(TLA_BUFFER_FILES)
+$(LOG)/TLA-Buffer.gz: $(OUT)/TLA $(TLA_BUFFER_FILES)
 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
 
-TLA_Memory: $(OUT)/TLA $(TLA_MEMORY_FILES)
+$(LOG)/TLA-Memory.gz: $(OUT)/TLA $(TLA_MEMORY_FILES)
 	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
 
 
@@ -115,7 +116,7 @@
 IOA_FILES = IOA/ROOT.ML IOA/Asig.thy IOA/Asig.ML IOA/IOA.thy \
   IOA/IOA.ML IOA/Solve.thy IOA/Solve.ML
 
-IOA: $(OUT)/HOL $(IOA_FILES)
+$(LOG)/HOL-IOA.gz: $(OUT)/HOL $(IOA_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL IOA
 
 
@@ -128,7 +129,7 @@
 
 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
 
-Auth:	$(OUT)/HOL $(AUTH_FILES)
+$(LOG)/HOL-Auth.gz: $(OUT)/HOL $(AUTH_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Auth
 
 
@@ -138,7 +139,7 @@
   Modelcheck/Example.thy Modelcheck/MCSyn.ML Modelcheck/MCSyn.thy \
   Modelcheck/MuCalculus.ML Modelcheck/MuCalculus.thy Modelcheck/ROOT.ML
 
-Modelcheck: $(OUT)/HOL $(MC_FILES)
+$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL $(MC_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
 
 
@@ -149,7 +150,7 @@
 SUBST_FILES = Subst/ROOT.ML \
 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
-Subst:	$(OUT)/HOL $(SUBST_FILES)
+$(LOG)/HOL-Subst.gz: $(OUT)/HOL $(SUBST_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Subst
 
 
@@ -160,7 +161,7 @@
 LAMBDA_FILES = Lambda/ROOT.ML \
 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
-Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
+$(LOG)/HOL-Lambda.gz: $(OUT)/HOL $(LAMBDA_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
 
 
@@ -171,7 +172,7 @@
 W0_FILES = W0/ROOT.ML \
 	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
 
-W0: $(OUT)/HOL $(W0_FILES)
+$(LOG)/HOL-W0.gz: $(OUT)/HOL $(W0_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL W0
 
 
@@ -182,7 +183,7 @@
 MINIML_FILES = MiniML/ROOT.ML \
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
-MiniML: $(OUT)/HOL $(MINIML_FILES)
+$(LOG)/HOL-MiniML.gz: $(OUT)/HOL $(MINIML_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL MiniML
 
 
@@ -193,7 +194,7 @@
 LEX_FILES = Lex/ROOT.ML \
 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
-Lex:	$(OUT)/HOL $(LEX_FILES)
+$(LOG)/HOL-Lex.gz: $(OUT)/HOL $(LEX_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 
@@ -212,15 +213,19 @@
 	ProductInsts.thy ROOT.ML Semigroup.thy Semigroups.thy Sigs.thy \
 	Xor.ML Xor.thy
 
-AXCLASSES_FILES = AxClasses/ROOT.ML \
-	$(AXC_GROUP_FILES:%=AxClasses/Group/%) \
-	$(AXC_LATTICE_FILES:%=AxClasses/Lattice/%) \
-	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
+$(LOG)/HOL-AxClasses.gz: AxClasses/ROOT.ML $(OUT)/HOL
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
+
+$(LOG)/HOL-AxClasses-Group.gz: $(LOG)/HOL-AxClasses.gz \
+  $(AXC_GROUP_FILES:%=AxClasses/Group/%)
+	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
 
-AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
-	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
-	@$(ISATOOL) usedir -s AxClasses-Group $(OUT)/HOL AxClasses/Group
+$(LOG)/HOL-AxClasses-Lattice.gz: $(LOG)/HOL-AxClasses.gz \
+  $(AXC_LATTICE_FILES:%=AxClasses/Lattice/%)
 	@$(ISATOOL) usedir -s AxClasses-Lattice $(OUT)/HOL AxClasses/Lattice
+
+$(LOG)/HOL-AxClasses-Tutorial.gz: $(LOG)/HOL-AxClasses.gz \
+  $(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
 	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
 
 
@@ -229,7 +234,8 @@
 QUOT_FILES = Quot/ROOT.ML Quot/PER0.thy Quot/PER0.ML Quot/PER.thy Quot/PER.ML \
 	Quot/HQUOT.thy Quot/HQUOT.ML Quot/NPAIR.thy Quot/NPAIR.ML \
 	Quot/FRACT.thy Quot/FRACT.ML
-Quot:	$(OUT)/HOL $(QUOT_FILES)
+
+$(LOG)/HOL-Quot.gz: $(OUT)/HOL $(QUOT_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL Quot
 
 
@@ -240,16 +246,25 @@
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
-ex:	$(OUT)/HOL $(EX_FILES)
+$(LOG)/HOL-ex.gz: $(OUT)/HOL $(EX_FILES)
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
 ## Full test
 
-test:	$(OUT)/HOL \
-	  Subst Induct IMP Hoare Lex Integ Auth Modelcheck Lambda  \
-	  W0 MiniML TLA TLA_Inc TLA_Buffer TLA_Memory IOA AxClasses Quot ex
-	echo 'Test examples ran successfully' > test
+ALL_TARGETS = $(OUT)/HOL $(LOG)/HOL-Subst.gz $(LOG)/HOL-Induct.gz \
+  $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz $(LOG)/HOL-Lex.gz \
+  $(LOG)/HOL-Integ.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-Modelcheck.gz \
+  $(LOG)/HOL-Lambda.gz $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
+  $(OUT)/TLA $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz \
+  $(LOG)/TLA-Memory.gz $(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses.gz \
+  $(LOG)/HOL-AxClasses-Group.gz $(LOG)/HOL-AxClasses-Lattice.gz \
+  $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz $(LOG)/HOL-ex.gz
+
+test: $(ALL_TARGETS)
+
+clean:
+	@rm -f $(ALL_TARGETS)
 
 
 .PRECIOUS: $(OUT)/Pure $(OUT)/HOL