isatool usedir;
authorwenzelm
Thu Mar 20 11:39:40 1997 +0100 (1997-03-20)
changeset 282813136dc7b9d0
parent 2827 cce436a62740
child 2829 c6b491e837cb
isatool usedir;
src/HOLCF/IsaMakefile
src/ZF/IsaMakefile
     1.1 --- a/src/HOLCF/IsaMakefile	Thu Mar 20 11:38:58 1997 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Thu Mar 20 11:39:40 1997 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
     1.5  
     1.6  $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
     1.7 -	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
     1.8 +	@$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF
     1.9  	@chmod -w $@
    1.10  
    1.11  $(OUT)/HOL:
    1.12 @@ -39,7 +39,7 @@
    1.13  IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
    1.14  
    1.15  IMP:	$(OUT)/HOLCF $(IMP_FILES)
    1.16 -	@$(ISATOOL) testdir $(OUT)/HOLCF IMP
    1.17 +	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
    1.18  
    1.19  ## Miscellaneous examples
    1.20  
    1.21 @@ -51,7 +51,7 @@
    1.22  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.23  
    1.24  EX:	ex/ROOT.ML $(EX_FILES)
    1.25 -	@$(ISATOOL) testdir $(OUT)/HOLCF ex
    1.26 +	@$(ISATOOL) usedir $(OUT)/HOLCF ex
    1.27  
    1.28  ## Full test
    1.29  
     2.1 --- a/src/ZF/IsaMakefile	Thu Mar 20 11:38:58 1997 +0100
     2.2 +++ b/src/ZF/IsaMakefile	Thu Mar 20 11:39:40 1997 +0100
     2.3 @@ -21,7 +21,7 @@
     2.4  	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
     2.5  
     2.6  $(OUT)/ZF: $(OUT)/FOL $(FILES)
     2.7 -	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/FOL ZF
     2.8 +	@$(ISATOOL) usedir -b -c $(OUT)/FOL ZF
     2.9  	@chmod -w $@
    2.10  
    2.11  $(OUT)/FOL:
    2.12 @@ -37,7 +37,7 @@
    2.13  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    2.14  
    2.15  IMP: $(OUT)/ZF $(IMP_FILES)
    2.16 -	@$(ISATOOL) testdir $(OUT)/ZF IMP
    2.17 +	@$(ISATOOL) usedir $(OUT)/ZF IMP
    2.18  
    2.19  
    2.20  ## Coinduction example
    2.21 @@ -48,7 +48,7 @@
    2.22  	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    2.23  
    2.24  Coind: $(OUT)/ZF $(COIND_FILES)
    2.25 -	@$(ISATOOL) testdir $(OUT)/ZF Coind
    2.26 +	@$(ISATOOL) usedir $(OUT)/ZF Coind
    2.27  
    2.28  
    2.29  ## AC examples
    2.30 @@ -64,7 +64,7 @@
    2.31  	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
    2.32  
    2.33  AC: $(OUT)/ZF $(AC_FILES)
    2.34 -	@$(ISATOOL) testdir $(OUT)/ZF AC
    2.35 +	@$(ISATOOL) usedir $(OUT)/ZF AC
    2.36  
    2.37  
    2.38  ## Residuals example
    2.39 @@ -75,7 +75,7 @@
    2.40  RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
    2.41  
    2.42  Resid: $(OUT)/ZF $(RESID_FILES)
    2.43 -	@$(ISATOOL) testdir $(OUT)/ZF Resid
    2.44 +	@$(ISATOOL) usedir $(OUT)/ZF Resid
    2.45  
    2.46  
    2.47  ## Miscellaneous examples
    2.48 @@ -86,7 +86,7 @@
    2.49  EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    2.50  
    2.51  ex: $(OUT)/ZF $(EX_FILES)
    2.52 -	@$(ISATOOL) testdir $(OUT)/ZF ex
    2.53 +	@$(ISATOOL) usedir $(OUT)/ZF ex
    2.54  
    2.55  
    2.56  ## Full test