src/HOL/IsaMakefile
changeset 2826 0b0d9e3bc661
parent 2635 835820c1591d
child 2827 cce436a62740
     1.1 --- a/src/HOL/IsaMakefile	Thu Mar 20 11:31:47 1997 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 20 11:32:57 1997 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
     1.5  
     1.6  $(OUT)/HOL: $(OUT)/Pure $(FILES)
     1.7 -	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu $(OUT)/Pure HOL
     1.8 +	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
     1.9  	@chmod -w $@
    1.10  
    1.11  $(OUT)/Pure:
    1.12 @@ -46,7 +46,7 @@
    1.13  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    1.14  
    1.15  IMP:	$(OUT)/HOL $(IMP_FILES)
    1.16 -	@$(ISATOOL) testdir $(OUT)/HOL IMP
    1.17 +	@$(ISATOOL) usedir $(OUT)/HOL IMP
    1.18  
    1.19  
    1.20  ## Hoare logic
    1.21 @@ -56,7 +56,7 @@
    1.22  	      $(Hoare_NAMES:%=Hoare/%.ML)
    1.23  
    1.24  Hoare:	$(OUT)/HOL $(Hoare_FILES)
    1.25 -	@$(ISATOOL) testdir $(OUT)/HOL Hoare
    1.26 +	@$(ISATOOL) usedir $(OUT)/HOL Hoare
    1.27  
    1.28  
    1.29  ## The integers in HOL
    1.30 @@ -67,7 +67,7 @@
    1.31  	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    1.32  
    1.33  Integ:	$(OUT)/HOL $(INTEG_FILES)
    1.34 -	@$(ISATOOL) testdir $(OUT)/HOL Integ
    1.35 +	@$(ISATOOL) usedir $(OUT)/HOL Integ
    1.36  
    1.37  
    1.38  ## I/O Automata
    1.39 @@ -86,8 +86,8 @@
    1.40   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    1.41  
    1.42  IOA:	$(OUT)/HOL $(IOA_FILES)
    1.43 -	@$(ISATOOL) testdir $(OUT)/HOL IOA/NTP
    1.44 -	@$(ISATOOL) testdir $(OUT)/HOL IOA/ABP
    1.45 +	@$(ISATOOL) usedir $(OUT)/HOL IOA/NTP
    1.46 +	@$(ISATOOL) usedir $(OUT)/HOL IOA/ABP
    1.47  
    1.48  
    1.49  ## Authentication & Security Protocols
    1.50 @@ -98,7 +98,7 @@
    1.51  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    1.52  
    1.53  Auth:	$(OUT)/HOL $(AUTH_FILES)
    1.54 -	@$(ISATOOL) testdir $(OUT)/HOL Auth
    1.55 +	@$(ISATOOL) usedir $(OUT)/HOL Auth
    1.56  
    1.57  
    1.58  ## Properties of substitutions
    1.59 @@ -109,7 +109,7 @@
    1.60  	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    1.61  
    1.62  Subst:	$(OUT)/HOL $(SUBST_FILES)
    1.63 -	@$(ISATOOL) testdir $(OUT)/HOL Subst
    1.64 +	@$(ISATOOL) usedir $(OUT)/HOL Subst
    1.65  
    1.66  
    1.67  ## Confluence of Lambda-calculus
    1.68 @@ -120,7 +120,7 @@
    1.69  	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    1.70  
    1.71  Lambda:	 $(OUT)/HOL $(LAMBDA_FILES)
    1.72 -	@$(ISATOOL) testdir $(OUT)/HOL Lambda
    1.73 +	@$(ISATOOL) usedir $(OUT)/HOL Lambda
    1.74  
    1.75  
    1.76  ## Type inference without let
    1.77 @@ -131,7 +131,7 @@
    1.78  	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
    1.79  
    1.80  W0: $(OUT)/HOL $(W0_FILES)
    1.81 -	@$(ISATOOL) testdir $(OUT)/HOL W0
    1.82 +	@$(ISATOOL) usedir $(OUT)/HOL W0
    1.83  
    1.84  
    1.85  ## Type inference with let
    1.86 @@ -142,7 +142,7 @@
    1.87  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    1.88  
    1.89  MiniML: $(OUT)/HOL $(MINIML_FILES)
    1.90 -	@$(ISATOOL) testdir $(OUT)/HOL MiniML
    1.91 +	@$(ISATOOL) usedir $(OUT)/HOL MiniML
    1.92  
    1.93  
    1.94  ## Lexical analysis
    1.95 @@ -153,7 +153,7 @@
    1.96  	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
    1.97  
    1.98  Lex:	$(OUT)/HOL $(LEX_FILES)
    1.99 -	@$(ISATOOL) testdir $(OUT)/HOL Lex
   1.100 +	@$(ISATOOL) usedir $(OUT)/HOL Lex
   1.101  
   1.102  
   1.103  ## Axiomatic type classes examples
   1.104 @@ -177,10 +177,10 @@
   1.105  	$(AXC_TUTORIAL_FILES:%=AxClasses/Tutorial/%)
   1.106  
   1.107  AxClasses: $(OUT)/HOL $(AXCLASSES_FILES)
   1.108 -	@$(ISATOOL) testdir $(OUT)/HOL AxClasses
   1.109 -	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Group
   1.110 -	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Lattice
   1.111 -	@$(ISATOOL) testdir $(OUT)/HOL AxClasses/Tutorial
   1.112 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   1.113 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Group
   1.114 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Lattice
   1.115 +	@$(ISATOOL) usedir $(OUT)/HOL AxClasses/Tutorial
   1.116  
   1.117  
   1.118  ## Miscellaneous examples
   1.119 @@ -192,7 +192,7 @@
   1.120  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   1.121  
   1.122  ex:	$(OUT)/HOL $(EX_FILES)
   1.123 -	@$(ISATOOL) testdir $(OUT)/HOL ex
   1.124 +	@$(ISATOOL) usedir $(OUT)/HOL ex
   1.125  
   1.126  
   1.127  ## Full test