src/HOL/IsaMakefile
changeset 28500 4b79e5d3d0aa
parent 28477 9339d4dcec8b
child 28592 824f8390aaa2
     1.1 --- a/src/HOL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4  HOL-Main: Pure $(OUT)/HOL-Main
     1.5  
     1.6  Pure:
     1.7 -	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     1.8 +	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
     1.9  
    1.10  $(OUT)/Pure: Pure
    1.11  
    1.12 @@ -182,7 +182,7 @@
    1.13    $(SRC)/Tools/rat.ML
    1.14  
    1.15  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
    1.16 -	@$(ISATOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    1.17 +	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    1.18  
    1.19  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    1.20    Arith_Tools.thy \
    1.21 @@ -247,7 +247,7 @@
    1.22    Tools/TFL/utils.ML
    1.23  
    1.24  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    1.25 -	@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    1.26 +	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    1.27  
    1.28  $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
    1.29    Complex/Complex_Main.thy \
    1.30 @@ -285,7 +285,7 @@
    1.31    Tools/Qelim/ferrante_rackoff.ML \
    1.32    Tools/Qelim/langford_data.ML \
    1.33    Tools/Qelim/langford.ML
    1.34 -	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    1.35 +	@$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
    1.36  
    1.37  
    1.38  ## HOL-Library
    1.39 @@ -320,7 +320,7 @@
    1.40    Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
    1.41    Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
    1.42    Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
    1.43 -	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
    1.44 +	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.45  
    1.46  
    1.47  ## HOL-HahnBanach
    1.48 @@ -337,7 +337,7 @@
    1.49    Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
    1.50    Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
    1.51    Real/HahnBanach/document/root.tex
    1.52 -	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL HahnBanach
    1.53 +	@cd Real; $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
    1.54  
    1.55  
    1.56  ## HOL-Subst
    1.57 @@ -346,7 +346,7 @@
    1.58  
    1.59  $(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
    1.60    Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
    1.61 -	@$(ISATOOL) usedir $(OUT)/HOL Subst
    1.62 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
    1.63  
    1.64  
    1.65  ## HOL-Induct
    1.66 @@ -359,7 +359,7 @@
    1.67    Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
    1.68    Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy		\
    1.69    Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
    1.70 -	@$(ISATOOL) usedir $(OUT)/HOL Induct
    1.71 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
    1.72  
    1.73  
    1.74  ## HOL-IMP
    1.75 @@ -370,7 +370,7 @@
    1.76    IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
    1.77    IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
    1.78    IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
    1.79 -	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
    1.80 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
    1.81  
    1.82  
    1.83  ## HOL-IMPP
    1.84 @@ -379,7 +379,7 @@
    1.85  
    1.86  $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
    1.87    IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
    1.88 -	@$(ISATOOL) usedir $(OUT)/HOL IMPP
    1.89 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
    1.90  
    1.91  
    1.92  ## HOL-Import
    1.93 @@ -397,7 +397,7 @@
    1.94  HOL-Import: HOL $(LOG)/HOL-Import.gz
    1.95  
    1.96  $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
    1.97 -	@$(ISATOOL) usedir $(OUT)/HOL Import
    1.98 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
    1.99  
   1.100  
   1.101  ## HOL-Generate-HOL
   1.102 @@ -410,7 +410,7 @@
   1.103    Import/Generate-HOL/GenHOL4Real.thy					\
   1.104    Import/Generate-HOL/GenHOL4Vec.thy					\
   1.105    Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
   1.106 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOL
   1.107 +	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
   1.108  
   1.109  
   1.110  ## HOL-Generate-HOLLight
   1.111 @@ -420,7 +420,7 @@
   1.112  $(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL		\
   1.113    $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
   1.114    Import/Generate-HOLLight/ROOT.ML
   1.115 -	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOLLight
   1.116 +	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
   1.117  
   1.118  
   1.119  ## HOL-Import-HOL
   1.120 @@ -443,14 +443,14 @@
   1.121    Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
   1.122    Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
   1.123    Import/HOL/ROOT.ML
   1.124 -	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL HOL4
   1.125 +	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
   1.126  
   1.127  HOLLight: HOL $(LOG)/HOLLight.gz
   1.128  
   1.129  $(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)	\
   1.130    Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
   1.131    Import/HOLLight/ROOT.ML
   1.132 -	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL HOLLight
   1.133 +	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
   1.134  
   1.135  
   1.136  ## HOL-NumberTheory
   1.137 @@ -468,7 +468,7 @@
   1.138    NumberTheory/Euler.thy NumberTheory/Gauss.thy				\
   1.139    NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
   1.140    NumberTheory/ROOT.ML
   1.141 -	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
   1.142 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
   1.143  
   1.144  
   1.145  ## HOL-Hoare
   1.146 @@ -481,7 +481,7 @@
   1.147    Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
   1.148    Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy	\
   1.149    Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
   1.150 -	@$(ISATOOL) usedir $(OUT)/HOL Hoare
   1.151 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
   1.152  
   1.153  
   1.154  ## HOL-HoareParallel
   1.155 @@ -498,7 +498,7 @@
   1.156    HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy			\
   1.157    HoareParallel/ROOT.ML HoareParallel/document/root.tex			\
   1.158    HoareParallel/document/root.bib
   1.159 -	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
   1.160 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HoareParallel
   1.161  
   1.162  
   1.163  ## HOL-MetisExamples
   1.164 @@ -510,7 +510,7 @@
   1.165    MetisExamples/BT.thy MetisExamples/Message.thy		\
   1.166    MetisExamples/Tarski.thy MetisExamples/TransClosure.thy	\
   1.167    MetisExamples/set.thy
   1.168 -	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
   1.169 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL MetisExamples
   1.170  
   1.171  
   1.172  ## HOL-Algebra
   1.173 @@ -533,7 +533,7 @@
   1.174    Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
   1.175    Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
   1.176    Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
   1.177 -	@cd Algebra; $(ISATOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
   1.178 +	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
   1.179  
   1.180  
   1.181  ## HOL-Auth
   1.182 @@ -557,7 +557,7 @@
   1.183    Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
   1.184    Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
   1.185    Auth/Smartcard/Smartcard.thy Auth/document/root.tex
   1.186 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
   1.187 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
   1.188  
   1.189  
   1.190  ## HOL-UNITY
   1.191 @@ -582,7 +582,7 @@
   1.192    UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
   1.193    UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
   1.194    UNITY/Comp/TimerArray.thy UNITY/document/root.tex
   1.195 -	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
   1.196 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
   1.197  
   1.198  
   1.199  ## HOL-Unix
   1.200 @@ -592,7 +592,7 @@
   1.201  $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy	\
   1.202    Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy		\
   1.203    Unix/document/root.bib Unix/document/root.tex
   1.204 -	@$(ISATOOL) usedir $(OUT)/HOL Unix
   1.205 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
   1.206  
   1.207  
   1.208  ## HOL-ZF
   1.209 @@ -601,7 +601,7 @@
   1.210  
   1.211  $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy	\
   1.212    ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
   1.213 -	@$(ISATOOL) usedir $(OUT)/HOL ZF
   1.214 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
   1.215  
   1.216  
   1.217  ## HOL-Modelcheck
   1.218 @@ -613,7 +613,7 @@
   1.219    Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy	\
   1.220    Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy		\
   1.221    Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
   1.222 -	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
   1.223 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
   1.224  
   1.225  
   1.226  ## HOL-SizeChange
   1.227 @@ -626,7 +626,7 @@
   1.228    SizeChange/Interpretation.thy SizeChange/Implementation.thy		\
   1.229    SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy	\
   1.230    SizeChange/sct.ML SizeChange/ROOT.ML
   1.231 -	@$(ISATOOL) usedir $(OUT)/HOL SizeChange
   1.232 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
   1.233  
   1.234  
   1.235  ## HOL-Lambda
   1.236 @@ -639,7 +639,7 @@
   1.237    Lambda/ParRed.thy Lambda/Standardization.thy Lambda/StrongNorm.thy	\
   1.238    Lambda/Type.thy Lambda/WeakNorm.thy Lambda/ROOT.ML			\
   1.239    Lambda/document/root.bib Lambda/document/root.tex
   1.240 -	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
   1.241 +	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
   1.242  
   1.243  
   1.244  ## HOL-Prolog
   1.245 @@ -648,7 +648,7 @@
   1.246  
   1.247  $(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
   1.248    Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
   1.249 -	@$(ISATOOL) usedir $(OUT)/HOL Prolog
   1.250 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
   1.251  
   1.252  
   1.253  ## HOL-W0
   1.254 @@ -656,7 +656,7 @@
   1.255  HOL-W0: HOL $(LOG)/HOL-W0.gz
   1.256  
   1.257  $(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
   1.258 -	@$(ISATOOL) usedir $(OUT)/HOL W0
   1.259 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL W0
   1.260  
   1.261  
   1.262  ## HOL-MicroJava
   1.263 @@ -692,7 +692,7 @@
   1.264    MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy			\
   1.265    MicroJava/document/root.bib MicroJava/document/root.tex		\
   1.266    MicroJava/document/introduction.tex
   1.267 -	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
   1.268 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
   1.269  
   1.270  
   1.271  ## HOL-NanoJava
   1.272 @@ -703,7 +703,7 @@
   1.273    NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
   1.274    NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
   1.275    NanoJava/document/root.bib NanoJava/document/root.tex
   1.276 -	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
   1.277 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
   1.278  
   1.279  
   1.280  ## HOL-Bali
   1.281 @@ -718,7 +718,7 @@
   1.282    Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
   1.283    Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
   1.284    Bali/WellType.thy Bali/document/root.tex
   1.285 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
   1.286 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
   1.287  
   1.288  
   1.289  ## HOL-Extraction
   1.290 @@ -731,7 +731,7 @@
   1.291    Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy	\
   1.292    Extraction/Warshall.thy Extraction/document/root.tex		\
   1.293    Extraction/document/root.bib
   1.294 -	@$(ISATOOL) usedir $(OUT)/HOL Extraction
   1.295 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Extraction
   1.296  
   1.297  
   1.298  ## HOL-IOA
   1.299 @@ -740,7 +740,7 @@
   1.300  
   1.301  $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
   1.302    IOA/Solve.thy
   1.303 -	@$(ISATOOL) usedir $(OUT)/HOL IOA
   1.304 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
   1.305  
   1.306  
   1.307  ## HOL-AxClasses
   1.308 @@ -749,7 +749,7 @@
   1.309  
   1.310  $(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
   1.311    AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
   1.312 -	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
   1.313 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
   1.314  
   1.315  
   1.316  ## HOL-Lattice
   1.317 @@ -759,7 +759,7 @@
   1.318  $(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
   1.319    Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
   1.320    Lattice/ROOT.ML Lattice/document/root.tex
   1.321 -	@$(ISATOOL) usedir $(OUT)/HOL Lattice
   1.322 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
   1.323  
   1.324  
   1.325  ## HOL-ex
   1.326 @@ -796,7 +796,7 @@
   1.327    Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
   1.328    Complex/ex/ReflectedFerrack.thy					\
   1.329    Complex/ex/linrtac.ML
   1.330 -	@$(ISATOOL) usedir $(OUT)/HOL ex
   1.331 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
   1.332  
   1.333  
   1.334  ## HOL-Isar_examples
   1.335 @@ -814,7 +814,7 @@
   1.336    Isar_examples/ROOT.ML Isar_examples/document/proof.sty		\
   1.337    Isar_examples/document/root.bib Isar_examples/document/root.tex	\
   1.338    Isar_examples/document/style.tex Hoare/hoare_tac.ML
   1.339 -	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
   1.340 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_examples
   1.341  
   1.342  
   1.343  ## HOL-SET-Protocol
   1.344 @@ -826,7 +826,7 @@
   1.345    SET-Protocol/PublicSET.thy SET-Protocol/Cardholder_Registration.thy	\
   1.346    SET-Protocol/Merchant_Registration.thy SET-Protocol/Purchase.thy	\
   1.347    SET-Protocol/document/root.tex
   1.348 -	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   1.349 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol
   1.350  
   1.351  
   1.352  ## HOL-Matrix
   1.353 @@ -847,7 +847,7 @@
   1.354    Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
   1.355    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
   1.356    Matrix/cplex/matrixlp.ML
   1.357 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
   1.358 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
   1.359  
   1.360  
   1.361  ## TLA
   1.362 @@ -856,7 +856,7 @@
   1.363  
   1.364  $(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
   1.365    TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
   1.366 -	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
   1.367 +	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
   1.368  
   1.369  
   1.370  ## TLA-Inc
   1.371 @@ -864,7 +864,7 @@
   1.372  TLA-Inc: TLA $(LOG)/TLA-Inc.gz
   1.373  
   1.374  $(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
   1.375 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
   1.376 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
   1.377  
   1.378  
   1.379  ## TLA-Buffer
   1.380 @@ -872,7 +872,7 @@
   1.381  TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
   1.382  
   1.383  $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
   1.384 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
   1.385 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
   1.386  
   1.387  
   1.388  ## TLA-Memory
   1.389 @@ -884,7 +884,7 @@
   1.390    TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
   1.391    TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
   1.392    TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
   1.393 -	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
   1.394 +	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
   1.395  
   1.396  
   1.397  ## HOL-Nominal
   1.398 @@ -902,7 +902,7 @@
   1.399    Nominal/nominal_primrec.ML \
   1.400    Nominal/nominal_thmdecls.ML \
   1.401    Library/Infinite_Set.thy
   1.402 -	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
   1.403 +	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
   1.404  
   1.405  
   1.406  ## HOL-Nominal-Examples
   1.407 @@ -931,7 +931,7 @@
   1.408    Nominal/Examples/VC_Condition.thy \
   1.409    Nominal/Examples/W.thy \
   1.410    Nominal/Examples/Weakening.thy
   1.411 -	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
   1.412 +	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
   1.413  
   1.414  
   1.415  ## HOL-Word
   1.416 @@ -946,7 +946,7 @@
   1.417    Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
   1.418    Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
   1.419    Word/document/root.bib
   1.420 -	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
   1.421 +	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
   1.422  
   1.423  
   1.424  ## HOL-Word-Examples
   1.425 @@ -955,7 +955,7 @@
   1.426  
   1.427  $(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
   1.428    Word/Examples/WordExamples.thy
   1.429 -	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
   1.430 +	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
   1.431  
   1.432  
   1.433  ## HOL-Statespace
   1.434 @@ -967,7 +967,7 @@
   1.435    Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy		\
   1.436    Statespace/distinct_tree_prover.ML Statespace/state_space.ML		\
   1.437    Statespace/state_fun.ML Statespace/document/root.tex
   1.438 -	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
   1.439 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
   1.440  
   1.441  
   1.442  ## HOL-NSA
   1.443 @@ -999,7 +999,7 @@
   1.444    Library/Infinite_Set.thy \
   1.445    Library/Zorn.thy \
   1.446    NSA/ROOT.ML
   1.447 -	@cd NSA; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
   1.448 +	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
   1.449  
   1.450  
   1.451  ## HOL-NSA-Examples
   1.452 @@ -1008,7 +1008,7 @@
   1.453  
   1.454  $(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML	\
   1.455    NSA/Examples/NSPrimes.thy
   1.456 -	@cd NSA; $(ISATOOL) usedir $(OUT)/HOL-NSA Examples
   1.457 +	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
   1.458  
   1.459  
   1.460  ## clean