--- a/src/HOL/IsaMakefile Fri Jun 01 23:21:40 2007 +0200
+++ b/src/HOL/IsaMakefile Fri Jun 01 23:33:49 2007 +0200
@@ -62,71 +62,71 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
- $(SRC)/Provers/Arith/assoc_fold.ML \
- $(SRC)/Provers/Arith/cancel_div_mod.ML \
- $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
- $(SRC)/Provers/Arith/cancel_numerals.ML \
- $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/combine_numerals.ML \
- $(SRC)/Provers/Arith/extract_common_term.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML \
- $(SRC)/Tools/IsaPlanner/isand.ML \
- $(SRC)/Tools/IsaPlanner/rw_inst.ML \
- $(SRC)/Tools/IsaPlanner/rw_tools.ML \
- $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML \
- $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
- $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \
- $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
- $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \
- $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML \
- ATP_Linkup.thy Accessible_Part.thy Code_Generator.thy Datatype.thy \
- Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy \
- FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \
- Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy \
- Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy \
- OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy \
- Presburger.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy \
- Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy \
- Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/reduce_axiomsN.ML \
- Tools/ATP/watcher.ML Tools/Presburger/cooper_dec.ML \
- Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML \
- Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML \
- Tools/Presburger/reflected_presburger.ML Tools/TFL/dcterm.ML \
- Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML \
- Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML \
- Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \
- Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML \
- Tools/datatype_hooks.ML Tools/datatype_package.ML \
- Tools/datatype_prop.ML Tools/datatype_realizer.ML \
- Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
- Tools/function_package/context_tree.ML \
- Tools/function_package/fundef_common.ML \
- Tools/function_package/fundef_core.ML \
- Tools/function_package/fundef_datatype.ML \
- Tools/function_package/fundef_lib.ML \
- Tools/function_package/fundef_package.ML \
- Tools/function_package/inductive_wrap.ML \
- Tools/function_package/lexicographic_order.ML \
- Tools/function_package/mutual.ML \
- Tools/function_package/pattern_split.ML \
- Tools/function_package/sum_tools.ML Tools/inductive_codegen.ML \
- Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \
- Tools/numeral_syntax.ML Tools/old_inductive_package.ML \
- Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \
- Tools/recdef_package.ML Tools/recfun_codegen.ML \
- Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \
- Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \
- Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \
- Tools/res_hol_clause.ML Tools/res_reconstruct.ML \
- Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \
- Tools/specification_package.ML Tools/split_rule.ML \
- Tools/string_syntax.ML Tools/typecopy_package.ML \
- Tools/typedef_codegen.ML Tools/typedef_package.ML \
- Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
- Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+ $(SRC)/Provers/Arith/assoc_fold.ML \
+ $(SRC)/Provers/Arith/cancel_div_mod.ML \
+ $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
+ $(SRC)/Provers/Arith/cancel_numerals.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/combine_numerals.ML \
+ $(SRC)/Provers/Arith/extract_common_term.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML \
+ $(SRC)/Tools/IsaPlanner/isand.ML \
+ $(SRC)/Tools/IsaPlanner/rw_inst.ML \
+ $(SRC)/Tools/IsaPlanner/rw_tools.ML \
+ $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML \
+ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
+ $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \
+ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
+ $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
+ $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \
+ $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML \
+ ATP_Linkup.thy Accessible_Part.thy Code_Generator.thy Datatype.thy \
+ Divides.thy Equiv_Relations.thy Extraction.thy Finite_Set.thy \
+ FixedPoint.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \
+ Inductive.thy IntArith.thy IntDef.thy IntDiv.thy Lattices.thy List.thy\
+ Main.thy Map.thy Nat.ML Nat.thy NatBin.thy NatSimprocs.thy Numeral.thy\
+ OrderedGroup.thy Orderings.thy Power.thy PreList.thy Predicate.thy \
+ Presburger.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+ Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy \
+ Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/reduce_axiomsN.ML \
+ Tools/ATP/watcher.ML Tools/Presburger/cooper_dec.ML \
+ Tools/Presburger/cooper_proof.ML Tools/Presburger/presburger.ML \
+ Tools/Presburger/qelim.ML Tools/Presburger/reflected_cooper.ML \
+ Tools/Presburger/reflected_presburger.ML Tools/TFL/dcterm.ML \
+ Tools/TFL/post.ML Tools/TFL/rules.ML Tools/TFL/tfl.ML \
+ Tools/TFL/thms.ML Tools/TFL/thry.ML Tools/TFL/usyntax.ML \
+ Tools/TFL/utils.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML \
+ Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML\
+ Tools/datatype_hooks.ML Tools/datatype_package.ML \
+ Tools/datatype_prop.ML Tools/datatype_realizer.ML \
+ Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
+ Tools/function_package/context_tree.ML \
+ Tools/function_package/fundef_common.ML \
+ Tools/function_package/fundef_core.ML \
+ Tools/function_package/fundef_datatype.ML \
+ Tools/function_package/fundef_lib.ML \
+ Tools/function_package/fundef_package.ML \
+ Tools/function_package/inductive_wrap.ML \
+ Tools/function_package/lexicographic_order.ML \
+ Tools/function_package/mutual.ML \
+ Tools/function_package/pattern_split.ML \
+ Tools/function_package/sum_tools.ML Tools/inductive_codegen.ML \
+ Tools/inductive_package.ML Tools/inductive_realizer.ML Tools/meson.ML \
+ Tools/numeral_syntax.ML Tools/old_inductive_package.ML \
+ Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \
+ Tools/recdef_package.ML Tools/recfun_codegen.ML \
+ Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \
+ Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \
+ Tools/res_atpset.ML Tools/res_axioms.ML Tools/res_clause.ML \
+ Tools/res_hol_clause.ML Tools/res_reconstruct.ML \
+ Tools/rewrite_hol_proof.ML Tools/sat_funcs.ML Tools/sat_solver.ML \
+ Tools/specification_package.ML Tools/split_rule.ML \
+ Tools/string_syntax.ML Tools/typecopy_package.ML \
+ Tools/typedef_codegen.ML Tools/typedef_package.ML \
+ Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy \
+ Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML \
int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
@@ -152,27 +152,28 @@
HOL-Complex: HOL $(OUT)/HOL-Complex
-$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Pure/General/float.ML \
- Library/Zorn.thy \
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Pure/General/float.ML \
+ Library/Zorn.thy \
Real/ContNotDenum.thy Real/Ferrante_Rackoff.thy Real/float_arith.ML \
- Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \
- Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy \
+ Real/Float.thy Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \
+ Real/ROOT.ML Real/Rational.thy Real/Real.thy Real/RealDef.thy \
Real/RealPow.thy Real/RealVector.thy Real/ferrante_rackoff_proof.ML \
- Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML \
- Hyperreal/StarDef.thy Hyperreal/StarClasses.thy \
- Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy \
- Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML \
- Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy \
- Hyperreal/HDeriv.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy \
- Hyperreal/Hyperreal.thy \
- Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy \
- Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy \
- Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy \
- Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
- Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy \
- Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML \
- Complex/Complex_Main.thy Complex/CLim.thy \
- Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy Complex/NSComplex.thy \
+ Real/ferrante_rackoff.ML Real/rat_arith.ML Real/real_arith.ML \
+ Hyperreal/StarDef.thy Hyperreal/StarClasses.thy \
+ Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy \
+ Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML \
+ Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy \
+ Hyperreal/HDeriv.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy \
+ Hyperreal/Hyperreal.thy \
+ Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy \
+ Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy \
+ Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy \
+ Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
+ Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy \
+ Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML \
+ Complex/Complex_Main.thy Complex/CLim.thy \
+ Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy \
+ Complex/NSComplex.thy \
Complex/document/root.tex Library/Infinite_Set.thy Library/Parity.thy
@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
@@ -183,7 +184,8 @@
$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
Complex/ex/ROOT.ML Complex/ex/document/root.tex \
- Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy Complex/ex/Ferrante_Rackoff_Ex.thy \
+ Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
+ Complex/ex/Ferrante_Rackoff_Ex.thy \
Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
@@ -194,11 +196,13 @@
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
- Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
+ Library/EfficientNat.thy Library/ExecutableSet.thy \
+ Library/ExecutableRat.thy \
Library/Executable_Real.thy \
Library/MLString.thy Library/Infinite_Set.thy \
Library/FuncSet.thy Library/Library.thy \
- Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy Library/NatPair.thy \
+ Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
+ Library/NatPair.thy \
Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
Library/Nat_Infinity.thy Library/Word.thy \
Library/README.html Library/Continuity.thy \
@@ -210,7 +214,8 @@
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
- Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
+ Library/SCT_Definition.thy Library/SCT_Theorem.thy \
+ Library/SCT_Interpretation.thy \
Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
Library/SCT_Examples.thy Library/sct.ML \
Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \
@@ -312,7 +317,8 @@
numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
- prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp rich_list.imp \
+ prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
+ rich_list.imp \
seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
word_base.imp word_bitop.imp word_num.imp
@@ -404,10 +410,12 @@
$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \
Auth/CertifiedEmail.thy Auth/Event.thy \
Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
- Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \
+ Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayReesBella.thy \
+ Auth/OtwayRees_AN.thy \
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
Auth/Recur.thy Auth/Shared.thy \
- Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy Auth/Kerberos_BAN_Gets.thy \
+ Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
+ Auth/Kerberos_BAN_Gets.thy \
Auth/KerberosIV.thy Auth/KerberosIV_Gets.thy Auth/KerberosV.thy \
Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
Auth/ZhouGollmann.thy \
@@ -416,9 +424,9 @@
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
Auth/Guard/P1.thy Auth/Guard/P2.thy \
- Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\
- Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy\
- Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy\
+ Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy \
+ Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy \
+ Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy \
Auth/document/root.tex
@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
@@ -482,7 +490,8 @@
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
- Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
+ 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/StrongNorm.thy Lambda/Type.thy \
Lambda/WeakNorm.thy Lambda/ROOT.ML \
@@ -494,7 +503,8 @@
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
-$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML Prolog/HOHH.thy \
+$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
+ Prolog/HOHH.thy \
Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
@$(ISATOOL) usedir $(OUT)/HOL Prolog
@@ -617,27 +627,27 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
-$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
- ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
- ex/BT.thy ex/BinEx.thy \
- ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
- ex/Eval_examples.thy ex/Random.thy \
- ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
- ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
- ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
- ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
- ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
- ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
- ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy \
- ex/LocaleTest2.thy ex/MT.ML \
- ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
- ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
- ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
- ex/Reflection.thy ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
- ex/Records.thy ex/Reflected_Presburger.thy ex/Refute_Examples.thy \
- ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
- ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
- ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML \
+$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
+ ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
+ ex/BT.thy ex/BinEx.thy \
+ ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \
+ ex/Eval_examples.thy ex/Random.thy \
+ ex/Codegenerator.thy ex/Codegenerator_Rat.thy \
+ ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
+ ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
+ ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
+ ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
+ ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
+ ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy \
+ ex/LocaleTest2.thy ex/MT.ML \
+ ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
+ ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
+ ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
+ ex/Reflection.thy ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
+ ex/Records.thy ex/Reflected_Presburger.thy ex/Refute_Examples.thy \
+ ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
+ ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
+ ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/reflection.ML \
ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
@$(ISATOOL) usedir $(OUT)/HOL ex
@@ -682,7 +692,8 @@
$(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
$(SRC)/Tools/Compute_Oracle/am_compiler.ML \
$(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
- $(SRC)/Tools/Compute_Oracle/am_util.ML $(SRC)/Tools/Compute_Oracle/compute.ML \
+ $(SRC)/Tools/Compute_Oracle/am_util.ML \
+ $(SRC)/Tools/Compute_Oracle/compute.ML \
Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
@@ -724,7 +735,8 @@
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \
TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.thy \
TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.thy \
- TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \
+ TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy \
+ TLA/Memory/RPC.thy \
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory