# 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