src/HOL/IsaMakefile

 HOL: Pure $(OUT)/HOL
 
 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
 
 
 ## HOL-Complex-HahnBanach

 
 ## HOL-Complex
 
 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
 
 
 ## HOL-Complex-ex
 
 HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
 
 $(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
 
 
 ## HOL-Library
 
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
 $(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 \
   Library/Nested_Environment.thy Library/Zorn.thy\
   Library/Library/ROOT.ML Library/Library/document/root.tex \

   Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
   Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
   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 \
   Library/Pretty_Char.thy Library/Pretty_Char_chr.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library

   bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
   hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
   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
 
 $(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
   $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \

 HOL-Auth: HOL $(LOG)/HOL-Auth.gz
 
 $(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 \
   Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
   Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
   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
 
 
 ## HOL-UNITY

 ## HOL-Lambda
 
 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 \
   Lambda/document/root.bib Lambda/document/root.tex
 	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda

 
 ## HOL-Prolog
 
 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
 
 
 ## HOL-W0

 
 ## HOL-ex
 
 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
 
 
 ## HOL-Isar_examples

 
 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   $(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 \
   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \

 TLA-Memory: TLA $(LOG)/TLA-Memory.gz
 
 $(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
 
 
 ## HOL-Nominal