# HG changeset patch
# User wenzelm
# Date 858854380 -3600
# Node ID 13136dc7b9d00d675615a78a1f78a67b3473193a
# Parent  cce436a62740cdacd13cd666a68206575e649569
isatool usedir;

diff -r cce436a62740 -r 13136dc7b9d0 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Mar 20 11:38:58 1997 +0100
+++ b/src/HOLCF/IsaMakefile	Thu Mar 20 11:39:40 1997 +0100
@@ -23,7 +23,7 @@
 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML)
 
 $(OUT)/HOLCF: $(OUT)/HOL $(FILES)
-	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/HOL HOLCF
+	@$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF
 	@chmod -w $@
 
 $(OUT)/HOL:
@@ -39,7 +39,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
 
 IMP:	$(OUT)/HOLCF $(IMP_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOLCF IMP
+	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
 
 ## Miscellaneous examples
 
@@ -51,7 +51,7 @@
 EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
 
 EX:	ex/ROOT.ML $(EX_FILES)
-	@$(ISATOOL) testdir $(OUT)/HOLCF ex
+	@$(ISATOOL) usedir $(OUT)/HOLCF ex
 
 ## Full test
 
diff -r cce436a62740 -r 13136dc7b9d0 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Thu Mar 20 11:38:58 1997 +0100
+++ b/src/ZF/IsaMakefile	Thu Mar 20 11:39:40 1997 +0100
@@ -21,7 +21,7 @@
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
 $(OUT)/ZF: $(OUT)/FOL $(FILES)
-	@$(ISABELLE) -e "make_html := $(ISABELLE_HTML);" -qu -c $(OUT)/FOL ZF
+	@$(ISATOOL) usedir -b -c $(OUT)/FOL ZF
 	@chmod -w $@
 
 $(OUT)/FOL:
@@ -37,7 +37,7 @@
 IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
 
 IMP: $(OUT)/ZF $(IMP_FILES)
-	@$(ISATOOL) testdir $(OUT)/ZF IMP
+	@$(ISATOOL) usedir $(OUT)/ZF IMP
 
 
 ## Coinduction example
@@ -48,7 +48,7 @@
 	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
 
 Coind: $(OUT)/ZF $(COIND_FILES)
-	@$(ISATOOL) testdir $(OUT)/ZF Coind
+	@$(ISATOOL) usedir $(OUT)/ZF Coind
 
 
 ## AC examples
@@ -64,7 +64,7 @@
 	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
 
 AC: $(OUT)/ZF $(AC_FILES)
-	@$(ISATOOL) testdir $(OUT)/ZF AC
+	@$(ISATOOL) usedir $(OUT)/ZF AC
 
 
 ## Residuals example
@@ -75,7 +75,7 @@
 RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) $(RESID_NAMES:%=Resid/%.ML)
 
 Resid: $(OUT)/ZF $(RESID_FILES)
-	@$(ISATOOL) testdir $(OUT)/ZF Resid
+	@$(ISATOOL) usedir $(OUT)/ZF Resid
 
 
 ## Miscellaneous examples
@@ -86,7 +86,7 @@
 EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex: $(OUT)/ZF $(EX_FILES)
-	@$(ISATOOL) testdir $(OUT)/ZF ex
+	@$(ISATOOL) usedir $(OUT)/ZF ex
 
 
 ## Full test