# HG changeset patch
# User wenzelm
# Date 858853977 -3600
# Node ID 0b0d9e3bc661dfee8c2ade132b29c6b5e9191aba
# Parent  a94dba60d5f2ccad63eb08a188a02018a1d550b8
isatool usedir;

diff -r a94dba60d5f2 -r 0b0d9e3bc661 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 20 11:31:47 1997 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 20 11:32:57 1997 +0100
@@ -20,7 +20,7 @@
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
 $(OUT)/HOL: $(OUT)/Pure $(FILES)
-	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL
+	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 	@chmod -w $@
 
 $(OUT)/Pure:
@@ -46,7 +46,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP:	$(OUT)/HOL $(IMP_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL IMP
+	@$(ISATOOL) usedir $(OUT)/HOL IMP
 
 
 ## Hoare logic
@@ -56,7 +56,7 @@
 	      $(Hoare_NAMES:%=Hoare/%.ML)
 
 Hoare:	$(OUT)/HOL $(Hoare_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Hoare
+	@$(ISATOOL) usedir $(OUT)/HOL Hoare
 
 
 ## The integers in HOL
@@ -67,7 +67,7 @@
 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
 Integ:	$(OUT)/HOL $(INTEG_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Integ
+	@$(ISATOOL) usedir $(OUT)/HOL Integ
 
 
 ## I/O Automata
@@ -86,8 +86,8 @@
  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
 
 IOA:	$(OUT)/HOL $(IOA_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL IOA/NTP
-	@$(ISATOOL) testdir $(OUT)/HOL IOA/ABP
+	@$(ISATOOL) usedir $(OUT)/HOL IOA/NTP
+	@$(ISATOOL) usedir $(OUT)/HOL IOA/ABP
 
 
 ## Authentication & Security Protocols
@@ -98,7 +98,7 @@
 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
 
 Auth:	$(OUT)/HOL $(AUTH_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Auth
+	@$(ISATOOL) usedir $(OUT)/HOL Auth
 
 
 ## Properties of substitutions
@@ -109,7 +109,7 @@
 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
 Subst:	$(OUT)/HOL $(SUBST_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Subst
+	@$(ISATOOL) usedir $(OUT)/HOL Subst
 
 
 ## Confluence of Lambda-calculus
@@ -120,7 +120,7 @@
 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
 Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Lambda
+	@$(ISATOOL) usedir $(OUT)/HOL Lambda
 
 
 ## Type inference without let
@@ -131,7 +131,7 @@
 	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
 
 W0: $(OUT)/HOL $(W0_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL W0
+	@$(ISATOOL) usedir $(OUT)/HOL W0
 
 
 ## Type inference with let
@@ -142,7 +142,7 @@
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
 MiniML: $(OUT)/HOL $(MINIML_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL MiniML
+	@$(ISATOOL) usedir $(OUT)/HOL MiniML
 
 
 ## Lexical analysis
@@ -153,7 +153,7 @@
 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
 Lex:	$(OUT)/HOL $(LEX_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL Lex
+	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 
 ## Axiomatic type classes examples
@@ -177,10 +177,10 @@
 	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
 
 AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL AxClasses
-	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Group
-	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Lattice
-	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Tutorial
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Group
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Lattice
+	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Tutorial
 
 
 ## Miscellaneous examples
@@ -192,7 +192,7 @@
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:	$(OUT)/HOL $(EX_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOL ex
+	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
 ## Full test