--- a/src/HOL/IsaMakefile Sat Oct 20 20:18:57 2001 +0200
+++ b/src/HOL/IsaMakefile Sat Oct 20 20:19:47 2001 +0200
@@ -172,7 +172,7 @@
Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
Real/HahnBanach/document/root.tex
- @cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real HahnBanach
+ @cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Real HahnBanach
## HOL-Library
@@ -248,7 +248,7 @@
NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
NumberTheory/ROOT.ML
- @$(ISATOOL) usedir $(OUT)/HOL NumberTheory
+ @$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
## HOL-GroupTheory
@@ -411,7 +411,7 @@
Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML Lambda/document/root.tex
- @$(ISATOOL) usedir $(OUT)/HOL Lambda
+ @$(ISATOOL) usedir -g true $(OUT)/HOL Lambda
## HOL-Prolog
@@ -466,7 +466,8 @@
MicroJava/BV/Step.thy MicroJava/BV/StepMono.thy \
MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
MicroJava/document/root.bib MicroJava/document/root.tex
- @$(ISATOOL) usedir $(OUT)/HOL MicroJava
+ @$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
+
## HOL-NanoJava
@@ -476,7 +477,8 @@
NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
NanoJava/document/root.bib NanoJava/document/root.tex
- @$(ISATOOL) usedir $(OUT)/HOL NanoJava
+ @$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
+
## HOL-CTL