# HG changeset patch # User wenzelm # Date 1213264307 -7200 # Node ID 81632fd4ff610a1a5e684b1faee30c8848843aa0 # Parent 587ad1fba128c3f26edeb20f3c04cfd31b8f797e some reformatting; diff -r 587ad1fba128 -r 81632fd4ff61 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jun 12 10:03:45 2008 +0200 +++ b/src/HOL/IsaMakefile Thu Jun 12 11:51:47 2008 +0200 @@ -78,46 +78,42 @@ $(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/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML \ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML $(SRC)/Provers/blast.ML \ - $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ - $(SRC)/Provers/order.ML \ + $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML \ + $(SRC)/Provers/blast.ML $(SRC)/Provers/clasimp.ML \ + $(SRC)/Provers/classical.ML $(SRC)/Provers/eqsubst.ML \ + $(SRC)/Provers/hypsubst.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)/Tools/Metis/metis.ML \ $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML \ - $(SRC)/Tools/code/code_target.ML \ - $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ - Arith_Tools.thy Code_Setup.thy Datatype.thy \ - Divides.thy Equiv_Relations.thy Extraction.thy \ - Finite_Set.thy Fun.thy FunDef.thy HOL.thy \ - Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \ - Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ - OrderedGroup.thy Orderings.thy Power.thy \ - Predicate.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 \ - Groebner_Basis.thy Tools/watcher.ML \ - Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ - Tools/Groebner_Basis/normalizer.ML \ + $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \ + $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \ + $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML \ + Tools/TFL/casesplit.ML ATP_Linkup.thy Arith_Tools.thy Code_Setup.thy \ + Datatype.thy Divides.thy Equiv_Relations.thy Extraction.thy \ + Finite_Set.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \ + Inductive.thy Int.thy IntDiv.thy Lattices.thy List.thy Main.thy \ + Map.thy Nat.thy NatBin.thy OrderedGroup.thy Orderings.thy Power.thy \ + Predicate.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 Groebner_Basis.thy \ + Tools/watcher.ML Tools/Groebner_Basis/groebner.ML \ + Tools/Groebner_Basis/misc.ML Tools/Groebner_Basis/normalizer.ML \ Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \ - Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \ + Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \ Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML \ Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML \ - Tools/Qelim/presburger.ML Tools/Qelim/qelim.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_package.ML \ + Tools/Qelim/presburger.ML Tools/Qelim/qelim.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_package.ML \ Tools/datatype_prop.ML Tools/datatype_realizer.ML \ - Tools/datatype_rep_proofs.ML Tools/dseq.ML \ - Tools/function_package/auto_term.ML \ + Tools/datatype_rep_proofs.ML Tools/dseq.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 \ @@ -126,26 +122,27 @@ Tools/function_package/fundef_package.ML \ Tools/function_package/inductive_wrap.ML \ Tools/function_package/lexicographic_order.ML \ - Tools/function_package/measure_functions.ML \ + Tools/function_package/measure_functions.ML \ Tools/function_package/mutual.ML \ - Tools/function_package/pattern_split.ML \ - Tools/function_package/size.ML Tools/induct_tacs.ML Tools/inductive_codegen.ML \ - Tools/inductive_package.ML Tools/inductive_realizer.ML \ - Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML \ - Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML \ - Tools/old_primrec_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_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/function_package/pattern_split.ML \ + Tools/function_package/size.ML Tools/induct_tacs.ML \ + Tools/inductive_codegen.ML Tools/inductive_package.ML \ + Tools/inductive_realizer.ML Tools/inductive_set_package.ML \ + Tools/lin_arith.ML Tools/meson.ML Tools/metis_tools.ML \ + Tools/numeral.ML Tools/numeral_syntax.ML \ + Tools/old_primrec_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_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.thy \ - arith_data.ML document/root.tex hologic.ML \ - int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML + Transitive_Closure.thy Typedef.thy Wellfounded.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 @@ -170,29 +167,27 @@ HOL-Complex: HOL $(OUT)/HOL-Complex -$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \ - Library/Zorn.thy Library/Order_Relation.thy \ - Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy \ - Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \ - Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy \ - Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML \ - Hyperreal/StarDef.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 Library/Univ_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/Fundamental_Theorem_Algebra.thy \ - Complex/CLim.thy \ +$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \ + Library/Zorn.thy Library/Order_Relation.thy Real/ContNotDenum.thy \ + Real/float_arith.ML Real/Float.thy Real/Lubs.thy Real/PReal.thy \ + Real/RComplete.thy Real/Rational.thy Real/Real.thy Real/RealDef.thy \ + Real/RealPow.thy Real/RealVector.thy Real/rat_arith.ML \ + Real/real_arith.ML Hyperreal/StarDef.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 \ + Library/Univ_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/Fundamental_Theorem_Algebra.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 + 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 @@ -200,12 +195,13 @@ 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/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \ - Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \ - Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML +$(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/NSPrimes.thy Complex/ex/Sqrt.thy \ + Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML \ + Complex/ex/mireif.ML Complex/ex/ReflectedFerrack.thy \ + Complex/ex/linreif.ML Complex/ex/linrtac.ML @cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex @@ -213,31 +209,32 @@ HOL-Library: HOL $(LOG)/HOL-Library.gz -$(LOG)/HOL-Library.gz: $(OUT)/HOL \ - Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \ - Library/Efficient_Nat.thy Library/Executable_Set.thy \ - Library/Infinite_Set.thy Library/Dense_Linear_Order.thy\ - Library/FuncSet.thy Library/Library.thy \ - Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \ - Library/NatPair.thy Library/Permutation.thy \ - Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \ - Library/Quicksort.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/Library/document/root.bib Library/While_Combinator.thy \ - Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \ - Library/Option_ord.thy Library/Sublist_Order.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/Eval.thy Library/Eval_Witness.thy \ - Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ - Library/Code_Integer.thy Library/Code_Message.thy \ - Library/Abstract_Rat.thy Library/Univ_Poly.thy\ - Library/Numeral_Type.thy Library/Boolean_Algebra.thy Library/Countable.thy \ - Library/RType.thy Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \ - Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy Library/Enum.thy +$(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy \ + Library/BigO.thy Library/Ramsey.thy Library/Efficient_Nat.thy \ + Library/Executable_Set.thy Library/Infinite_Set.thy \ + Library/Dense_Linear_Order.thy Library/FuncSet.thy \ + Library/Library.thy Library/List_Prefix.thy Library/State_Monad.thy \ + Library/Multiset.thy Library/NatPair.thy Library/Permutation.thy \ + Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \ + Library/Quicksort.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/Library/document/root.bib Library/While_Combinator.thy \ + Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \ + Library/Option_ord.thy Library/Sublist_Order.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/Eval.thy Library/Eval_Witness.thy \ + Library/Code_Index.thy Library/Code_Char.thy \ + Library/Code_Char_chr.thy Library/Code_Integer.thy \ + Library/Code_Message.thy Library/Abstract_Rat.thy \ + Library/Univ_Poly.thy Library/Numeral_Type.thy \ + Library/Boolean_Algebra.thy Library/Countable.thy Library/RType.thy \ + Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \ + Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy \ + Library/Enum.thy @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library @@ -245,9 +242,8 @@ HOL-Subst: HOL $(LOG)/HOL-Subst.gz -$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \ - Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \ - Subst/Unify.thy +$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \ + Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy @$(ISATOOL) usedir $(OUT)/HOL Subst @@ -255,14 +251,12 @@ HOL-Induct: HOL $(LOG)/HOL-Induct.gz -$(LOG)/HOL-Induct.gz: $(OUT)/HOL \ - Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \ - Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \ - Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\ - Induct/ROOT.ML \ - Induct/Sexp.thy Induct/Sigma_Algebra.thy \ - Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \ - Induct/Tree.thy Induct/document/root.tex +$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ + Induct/LFilter.thy Induct/LList.thy Induct/Mutil.thy \ + Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \ + Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ + Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy \ + Induct/Term.thy Induct/Tree.thy Induct/document/root.tex @$(ISATOOL) usedir $(OUT)/HOL Induct @@ -270,11 +264,10 @@ HOL-IMP: HOL $(LOG)/HOL-IMP.gz -$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \ - IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \ - IMP/Natural.thy IMP/Examples.thy \ - IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \ - IMP/document/root.bib +$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \ + IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \ + IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \ + IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib @$(ISATOOL) usedir -g true $(OUT)/HOL IMP @@ -282,7 +275,7 @@ HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz -$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ +$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy @$(ISATOOL) usedir $(OUT)/HOL IMPP @@ -309,9 +302,11 @@ HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz -$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \ - Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \ - Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy \ +$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex \ + $(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \ + Import/Generate-HOL/GenHOL4Prob.thy \ + Import/Generate-HOL/GenHOL4Real.thy \ + Import/Generate-HOL/GenHOL4Vec.thy \ Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL @@ -320,8 +315,9 @@ HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz -$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \ - Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML +$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex \ + $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \ + Import/Generate-HOLLight/ROOT.ML @cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight @@ -340,16 +336,17 @@ 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 \ - Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \ - Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML +$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \ + $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ + Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \ + Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \ + Import/HOL/ROOT.ML @cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4 HOLLight: HOL-Complex $(LOG)/HOLLight.gz -$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \ - Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ +$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \ + Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ Import/HOLLight/ROOT.ML @cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight @@ -358,15 +355,16 @@ HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz -$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ - Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \ - NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \ - NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \ - NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \ - NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \ - NumberTheory/Finite2.thy NumberTheory/Int2.thy NumberTheory/EvenOdd.thy\ - NumberTheory/Residues.thy NumberTheory/Euler.thy NumberTheory/Gauss.thy\ - NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy\ +$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL Library/Permutation.thy \ + Library/Primes.thy NumberTheory/Fib.thy \ + NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \ + NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \ + NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \ + NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \ + NumberTheory/Finite2.thy NumberTheory/Int2.thy \ + NumberTheory/EvenOdd.thy NumberTheory/Residues.thy \ + NumberTheory/Euler.thy NumberTheory/Gauss.thy \ + NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ NumberTheory/ROOT.ML @$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory @@ -375,13 +373,12 @@ HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz -$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \ - Hoare/Examples.thy Hoare/Hoare.thy Hoare/hoare_tac.ML \ - Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \ - Hoare/ROOT.ML Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ - Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \ - Hoare/Separation.thy Hoare/SepLogHeap.thy \ - Hoare/document/root.tex Hoare/document/root.bib +$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ + Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \ + Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ + Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ + Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \ + Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib @$(ISATOOL) usedir $(OUT)/HOL Hoare @@ -389,16 +386,16 @@ HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz -$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \ - HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy \ - HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy \ - HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy \ - HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy \ - HoareParallel/Quote_Antiquote.thy \ - HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy \ - HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy \ - HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML \ - HoareParallel/document/root.tex HoareParallel/document/root.bib +$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \ + HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy \ + HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy \ + HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy \ + HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy \ + HoareParallel/Quote_Antiquote.thy HoareParallel/RG_Com.thy \ + HoareParallel/RG_Examples.thy HoareParallel/RG_Hoare.thy \ + HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy \ + HoareParallel/ROOT.ML HoareParallel/document/root.tex \ + HoareParallel/document/root.bib @$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel @@ -406,10 +403,10 @@ HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz -$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \ - MetisExamples/ROOT.ML \ - MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \ - MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \ +$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL MetisExamples/ROOT.ML \ + MetisExamples/Abstraction.thy MetisExamples/BigO.thy \ + MetisExamples/BT.thy MetisExamples/Message.thy \ + MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \ MetisExamples/set.thy @$(ISATOOL) usedir $(OUT)/HOL MetisExamples @@ -437,27 +434,23 @@ 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/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/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/document/root.tex +$(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/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/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/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL Auth @@ -465,23 +458,24 @@ HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz -$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ - UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \ - UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ - UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\ - UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\ - UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\ - UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \ - UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \ - UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ - UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\ - UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\ - UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy \ - UNITY/Comp/Client.thy UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ - UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ - UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ - UNITY/Comp/TimerArray.thy\ - UNITY/document/root.tex +$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ + UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \ + UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ + UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ + UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ + UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ + UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ + UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \ + UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \ + UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ + UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \ + UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \ + UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \ + UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ + UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ + UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ + UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ + UNITY/Comp/TimerArray.thy UNITY/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL UNITY @@ -489,8 +483,8 @@ HOL-Unix: HOL $(LOG)/HOL-Unix.gz -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ - Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ +$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ + Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ Unix/document/root.bib Unix/document/root.tex @$(ISATOOL) usedir $(OUT)/HOL Unix @@ -498,19 +492,18 @@ HOL-ZF: HOL $(LOG)/HOL-ZF.gz -$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML \ - ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \ - ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex +$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy \ + ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex @$(ISATOOL) usedir $(OUT)/HOL ZF ## HOL-Modelcheck HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz -$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ - Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ - Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ - Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ +$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \ + Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \ + Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \ + Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \ Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML @$(ISATOOL) usedir $(OUT)/HOL Modelcheck @@ -518,26 +511,23 @@ HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz -$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL \ - SizeChange/Kleene_Algebras.thy SizeChange/Graphs.thy \ - SizeChange/Misc_Tools.thy SizeChange/Criterion.thy \ - SizeChange/Correctness.thy SizeChange/Interpretation.thy \ - SizeChange/Implementation.thy SizeChange/Size_Change_Termination.thy \ - SizeChange/Examples.thy SizeChange/sct.ML \ - SizeChange/ROOT.ML +$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL SizeChange/Kleene_Algebras.thy \ + SizeChange/Graphs.thy SizeChange/Misc_Tools.thy \ + SizeChange/Criterion.thy SizeChange/Correctness.thy \ + SizeChange/Interpretation.thy SizeChange/Implementation.thy \ + SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy \ + SizeChange/sct.ML SizeChange/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL SizeChange ## 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/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \ - Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \ - Lambda/StrongNorm.thy Lambda/Type.thy \ - Lambda/WeakNorm.thy Lambda/ROOT.ML \ +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.thy Lambda/Eta.thy \ + Lambda/InductTermi.thy Lambda/Lambda.thy Lambda/ListApplication.thy \ + Lambda/ListBeta.thy Lambda/ListOrder.thy Lambda/NormalForm.thy \ + Lambda/ParRed.thy Lambda/Standardization.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 @@ -546,9 +536,8 @@ HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz -$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \ - Prolog/HOHH.thy \ - Prolog/Test.thy Prolog/Func.thy Prolog/Type.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 @@ -564,38 +553,34 @@ HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz -$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \ - MicroJava/ROOT.ML \ - MicroJava/Comp/AuxLemmas.thy \ - MicroJava/Comp/CorrComp.thy \ - MicroJava/Comp/CorrCompTp.thy \ - MicroJava/Comp/DefsComp.thy \ - MicroJava/Comp/Index.thy \ - MicroJava/Comp/LemmasComp.thy \ - MicroJava/Comp/NatCanonify.thy \ - MicroJava/Comp/TranslComp.thy \ - MicroJava/Comp/TranslCompTp.thy \ - MicroJava/Comp/TypeInf.thy \ - MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ - MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ - MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ - MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ - MicroJava/J/WellType.thy MicroJava/J/Example.thy \ - MicroJava/J/JListExample.thy \ - MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\ - MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\ - MicroJava/JVM/JVMListExample.thy MicroJava/JVM/JVMExceptions.thy \ - MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpecTypeSafe.thy \ - MicroJava/BV/Correct.thy MicroJava/BV/Err.thy MicroJava/BV/JType.thy \ - MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy MicroJava/BV/Kildall.thy \ - MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \ - MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \ - MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ - MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \ - MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \ - MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \ - MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \ - MicroJava/document/root.bib MicroJava/document/root.tex \ +$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \ + MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \ + MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \ + MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \ + MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \ + MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ + MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ + MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ + MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ + MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ + MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ + MicroJava/J/WellType.thy MicroJava/J/Example.thy \ + MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \ + MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \ + MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy \ + MicroJava/JVM/JVMExceptions.thy MicroJava/BV/BVSpec.thy \ + MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy \ + MicroJava/BV/Err.thy MicroJava/BV/JType.thy MicroJava/BV/JVM.thy \ + MicroJava/BV/JVMType.thy MicroJava/BV/Kildall.thy \ + MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \ + MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \ + MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ + MicroJava/BV/Typing_Framework.thy \ + MicroJava/BV/Typing_Framework_err.thy \ + MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \ + MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \ + MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \ + MicroJava/document/root.bib MicroJava/document/root.tex \ MicroJava/document/introduction.tex @$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava @@ -604,9 +589,9 @@ HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz -$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \ - NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \ - NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ +$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML 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 -g true $(OUT)/HOL NanoJava @@ -621,7 +606,7 @@ Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \ Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy \ Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy \ - Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \ + Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \ Bali/WellType.thy Bali/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL Bali @@ -630,11 +615,11 @@ HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz -$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \ - Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy \ - Extraction/Higman.thy Extraction/Pigeonhole.thy Extraction/QuotRem.thy \ - Extraction/ROOT.ML Extraction/Util.thy \ - Extraction/Warshall.thy Extraction/document/root.tex \ +$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \ + Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy \ + Extraction/Higman.thy Extraction/Pigeonhole.thy \ + Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy \ + Extraction/Warshall.thy Extraction/document/root.tex \ Extraction/document/root.bib @$(ISATOOL) usedir $(OUT)/HOL Extraction @@ -643,8 +628,8 @@ HOL-IOA: HOL $(LOG)/HOL-IOA.gz -$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \ - IOA/ROOT.ML IOA/Solve.thy +$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ + IOA/Solve.thy @$(ISATOOL) usedir $(OUT)/HOL IOA @@ -652,7 +637,7 @@ HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz -$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \ +$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \ AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy @$(ISATOOL) usedir $(OUT)/HOL AxClasses @@ -661,8 +646,8 @@ HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz -$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ - Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \ +$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ + Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \ Lattice/ROOT.ML Lattice/document/root.tex @$(ISATOOL) usedir $(OUT)/HOL Lattice @@ -671,28 +656,28 @@ 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/CTL.thy \ - ex/Chinese.thy ex/Classical.thy ex/Dense_Linear_Order_Ex.thy \ - ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy \ - ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ - ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.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/Induction_Scheme.thy \ - ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ - ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \ - 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/Quickcheck_Examples.thy \ - ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \ - ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \ - ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ - ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \ - ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \ - ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy +$(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/CTL.thy ex/Chinese.thy ex/Classical.thy \ + ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy \ + ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy \ + ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ + ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.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/Induction_Scheme.thy ex/InductiveInvariant.thy \ + ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ + ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy 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/Quickcheck_Examples.thy ex/Reflection.thy ex/reflection_data.ML \ + ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ + ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \ + ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ + ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \ + ex/document/root.tex ex/Meson_Test.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 @@ -700,15 +685,16 @@ HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz -$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \ - Isar_examples/Cantor.thy Isar_examples/Drinker.thy \ - Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \ - Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \ - Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \ - Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \ - Isar_examples/Puzzle.thy Isar_examples/Summation.thy \ - Isar_examples/ROOT.ML Isar_examples/document/proof.sty \ - Isar_examples/document/root.bib Isar_examples/document/root.tex \ +$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \ + Isar_examples/Cantor.thy Isar_examples/Drinker.thy \ + Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \ + Isar_examples/Group.thy Isar_examples/Hoare.thy \ + Isar_examples/HoareEx.thy Isar_examples/KnasterTarski.thy \ + Isar_examples/MutilatedCheckerboard.thy \ + Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \ + Isar_examples/Puzzle.thy Isar_examples/Summation.thy \ + Isar_examples/ROOT.ML Isar_examples/document/proof.sty \ + Isar_examples/document/root.bib Isar_examples/document/root.tex \ Isar_examples/document/style.tex Hoare/hoare_tac.ML @$(ISATOOL) usedir $(OUT)/HOL Isar_examples @@ -717,14 +703,11 @@ HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz -$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \ - SET-Protocol/MessageSET.thy\ - SET-Protocol/EventSET.thy\ - SET-Protocol/PublicSET.thy\ - SET-Protocol/Cardholder_Registration.thy\ - SET-Protocol/Merchant_Registration.thy\ - SET-Protocol/Purchase.thy\ - SET-Protocol/document/root.tex +$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \ + SET-Protocol/MessageSET.thy SET-Protocol/EventSET.thy \ + SET-Protocol/PublicSET.thy SET-Protocol/Cardholder_Registration.thy \ + SET-Protocol/Merchant_Registration.thy SET-Protocol/Purchase.thy \ + SET-Protocol/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol @@ -732,20 +715,20 @@ HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix -$(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.ML \ - $(SRC)/Tools/Compute_Oracle/linker.ML \ - $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ - $(SRC)/Tools/Compute_Oracle/am_sml.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 \ +$(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.ML \ + $(SRC)/Tools/Compute_Oracle/linker.ML \ + $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ + $(SRC)/Tools/Compute_Oracle/am_sml.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 \ Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML @cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix @@ -754,7 +737,7 @@ TLA: HOL $(OUT)/TLA -$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ +$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy @cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA @@ -779,11 +762,10 @@ TLA-Memory: TLA $(LOG)/TLA-Memory.gz -$(LOG)/TLA-Memory.gz: $(OUT)/TLA \ - 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 \ +$(LOG)/TLA-Memory.gz: $(OUT)/TLA 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/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy @cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory @@ -838,23 +820,14 @@ HOL-Word: HOL $(OUT)/HOL-Word -$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \ - Library/Infinite_Set.thy Library/Parity.thy \ - Library/Boolean_Algebra.thy Library/Numeral_Type.thy \ - Word/Num_Lemmas.thy \ - Word/TdThs.thy \ - Word/Size.thy \ - Word/BinGeneral.thy \ - Word/BinOperations.thy \ - Word/BinBoolList.thy \ - Word/BitSyntax.thy \ - Word/WordDefinition.thy \ - Word/WordArith.thy \ - Word/WordBitwise.thy \ - Word/WordShift.thy \ - Word/WordGenLib.thy \ - Word/WordMain.thy \ - Word/document/root.tex Word/document/root.bib +$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Infinite_Set.thy \ + Library/Parity.thy Library/Boolean_Algebra.thy \ + Library/Numeral_Type.thy Word/Num_Lemmas.thy Word/TdThs.thy \ + Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy \ + Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy \ + Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy \ + Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex \ + Word/document/root.bib @cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word @@ -862,8 +835,7 @@ HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz -$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word \ - Word/Examples/ROOT.ML \ +$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \ Word/Examples/WordExamples.thy @cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples @@ -871,12 +843,11 @@ HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz -$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \ - Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \ - Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \ - Statespace/distinct_tree_prover.ML Statespace/state_space.ML \ - Statespace/state_fun.ML \ - Statespace/document/root.tex +$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \ + Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \ + Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \ + Statespace/distinct_tree_prover.ML Statespace/state_space.ML \ + Statespace/state_fun.ML Statespace/document/root.tex @$(ISATOOL) usedir -g true $(OUT)/HOL Statespace ## clean