--- 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