# HG changeset patch # User wenzelm # Date 1345668941 -7200 # Node ID c0eafbd55de3fc679eb6100d4de2f3aa57a60182 # Parent d72ca5742f80e27eefffe76ae6bed08afd042b4f prefer ML_file over old uses; diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/Classes/Thy/Setup.thy --- a/doc-src/Classes/Thy/Setup.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/Classes/Thy/Setup.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,10 +1,10 @@ theory Setup imports Main "~~/src/HOL/Library/Code_Integer" -uses - "../../antiquote_setup.ML" - "../../more_antiquote.ML" begin +ML_file "../../antiquote_setup.ML" +ML_file "../../more_antiquote.ML" + setup {* Antiquote_Setup.setup #> More_Antiquote.setup #> diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,11 +4,11 @@ "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/RBT" "~~/src/HOL/Library/Mapping" -uses - "../../antiquote_setup.ML" - "../../more_antiquote.ML" begin +ML_file "../../antiquote_setup.ML" +ML_file "../../more_antiquote.ML" + setup {* Antiquote_Setup.setup #> More_Antiquote.setup #> diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/IsarImplementation/Thy/Base.thy --- a/doc-src/IsarImplementation/Thy/Base.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/IsarImplementation/Thy/Base.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,8 +1,8 @@ theory Base imports Main -uses "../../antiquote_setup.ML" begin +ML_file "../../antiquote_setup.ML" setup {* Antiquote_Setup.setup *} end diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/IsarRef/Thy/Base.thy --- a/doc-src/IsarRef/Thy/Base.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/IsarRef/Thy/Base.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,8 +1,9 @@ theory Base imports Pure -uses "../../antiquote_setup.ML" begin +ML_file "../../antiquote_setup.ML" + setup {* Antiquote_Setup.setup #> member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/System/Thy/Base.thy --- a/doc-src/System/Thy/Base.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/System/Thy/Base.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,9 +1,9 @@ theory Base imports Pure -uses "../../antiquote_setup.ML" begin -setup {* Antiquote_Setup.setup *} +ML_file "../../antiquote_setup.ML" +setup Antiquote_Setup.setup declare [[thy_output_source]] diff -r d72ca5742f80 -r c0eafbd55de3 doc-src/TutorialI/Types/Setup.thy --- a/doc-src/TutorialI/Types/Setup.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/doc-src/TutorialI/Types/Setup.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,11 +1,10 @@ theory Setup imports Main -uses - "../../antiquote_setup.ML" - "../../more_antiquote.ML" begin +ML_file "../../antiquote_setup.ML" +ML_file "../../more_antiquote.ML" + setup {* Antiquote_Setup.setup #> More_Antiquote.setup *} - end \ No newline at end of file diff -r d72ca5742f80 -r c0eafbd55de3 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/CTT/CTT.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,9 @@ theory CTT imports Pure -uses "~~/src/Provers/typedsimp.ML" ("rew.ML") begin +ML_file "~~/src/Provers/typedsimp.ML" setup Pure_Thy.old_appl_syntax_setup typedecl i @@ -460,7 +460,7 @@ fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms) *} -use "rew.ML" +ML_file "rew.ML" subsection {* The elimination rules for fst/snd *} diff -r d72ca5742f80 -r c0eafbd55de3 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/FOL/FOL.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,15 +7,14 @@ theory FOL imports IFOL keywords "print_claset" "print_induct_rules" :: diag -uses - "~~/src/Provers/classical.ML" - "~~/src/Provers/blast.ML" - "~~/src/Provers/clasimp.ML" - "~~/src/Tools/induct.ML" - "~~/src/Tools/case_product.ML" - ("simpdata.ML") begin +ML_file "~~/src/Provers/classical.ML" +ML_file "~~/src/Provers/blast.ML" +ML_file "~~/src/Provers/clasimp.ML" +ML_file "~~/src/Tools/induct.ML" +ML_file "~~/src/Tools/case_product.ML" + subsection {* The classical axiom *} @@ -329,7 +328,7 @@ not_imp not_all not_ex cases_simp cla_simps_misc -use "simpdata.ML" +ML_file "simpdata.ML" simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *} simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *} diff -r d72ca5742f80 -r c0eafbd55de3 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/FOL/IFOL.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,23 +6,21 @@ theory IFOL imports Pure -uses - "~~/src/Tools/misc_legacy.ML" - "~~/src/Provers/splitter.ML" - "~~/src/Provers/hypsubst.ML" - "~~/src/Tools/IsaPlanner/zipper.ML" - "~~/src/Tools/IsaPlanner/isand.ML" - "~~/src/Tools/IsaPlanner/rw_tools.ML" - "~~/src/Tools/IsaPlanner/rw_inst.ML" - "~~/src/Tools/eqsubst.ML" - "~~/src/Provers/quantifier1.ML" - "~~/src/Tools/intuitionistic.ML" - "~~/src/Tools/project_rule.ML" - "~~/src/Tools/atomize_elim.ML" - ("fologic.ML") - ("intprover.ML") begin +ML_file "~~/src/Tools/misc_legacy.ML" +ML_file "~~/src/Provers/splitter.ML" +ML_file "~~/src/Provers/hypsubst.ML" +ML_file "~~/src/Tools/IsaPlanner/zipper.ML" +ML_file "~~/src/Tools/IsaPlanner/isand.ML" +ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML" +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" +ML_file "~~/src/Tools/eqsubst.ML" +ML_file "~~/src/Provers/quantifier1.ML" +ML_file "~~/src/Tools/intuitionistic.ML" +ML_file "~~/src/Tools/project_rule.ML" +ML_file "~~/src/Tools/atomize_elim.ML" + subsection {* Syntax and axiomatic basis *} @@ -575,7 +573,7 @@ ) *} -use "fologic.ML" +ML_file "fologic.ML" lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" . @@ -597,7 +595,7 @@ *} setup hypsubst_setup -use "intprover.ML" +ML_file "intprover.ML" subsection {* Intuitionistic Reasoning *} diff -r d72ca5742f80 -r c0eafbd55de3 src/FOLP/FOLP.thy --- a/src/FOLP/FOLP.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/FOLP/FOLP.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,8 +7,6 @@ theory FOLP imports IFOLP -uses - ("classical.ML") ("simp.ML") ("simpdata.ML") begin axiomatization cla :: "[p=>p]=>p" @@ -99,8 +97,8 @@ apply assumption done -use "classical.ML" (* Patched 'cos matching won't instantiate proof *) -use "simp.ML" (* Patched 'cos matching won't instantiate proof *) +ML_file "classical.ML" (* Patched because matching won't instantiate proof *) +ML_file "simp.ML" (* Patched because matching won't instantiate proof *) ML {* structure Cla = Classical @@ -139,6 +137,6 @@ apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *}) done -use "simpdata.ML" +ML_file "simpdata.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/FOLP/IFOLP.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,10 @@ theory IFOLP imports Pure -uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML") begin +ML_file "~~/src/Tools/misc_legacy.ML" + setup Pure_Thy.old_appl_syntax_setup classes "term" @@ -587,7 +588,7 @@ lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" . -use "hypsubst.ML" +ML_file "hypsubst.ML" ML {* structure Hypsubst = Hypsubst @@ -609,7 +610,7 @@ open Hypsubst; *} -use "intprover.ML" +ML_file "intprover.ML" (*** Rewrite rules ***) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/ATP.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,17 +7,15 @@ theory ATP imports Meson -uses "Tools/lambda_lifting.ML" - "Tools/monomorph.ML" - "Tools/ATP/atp_util.ML" - "Tools/ATP/atp_problem.ML" - "Tools/ATP/atp_proof.ML" - "Tools/ATP/atp_proof_redirect.ML" - ("Tools/ATP/atp_problem_generate.ML") - ("Tools/ATP/atp_proof_reconstruct.ML") - ("Tools/ATP/atp_systems.ML") begin +ML_file "Tools/lambda_lifting.ML" +ML_file "Tools/monomorph.ML" +ML_file "Tools/ATP/atp_util.ML" +ML_file "Tools/ATP/atp_problem.ML" +ML_file "Tools/ATP/atp_proof.ML" +ML_file "Tools/ATP/atp_proof_redirect.ML" + subsection {* Higher-order reasoning helpers *} definition fFalse :: bool where [no_atp]: @@ -132,9 +130,9 @@ subsection {* Setup *} -use "Tools/ATP/atp_problem_generate.ML" -use "Tools/ATP/atp_proof_reconstruct.ML" -use "Tools/ATP/atp_systems.ML" +ML_file "Tools/ATP/atp_problem_generate.ML" +ML_file "Tools/ATP/atp_proof_reconstruct.ML" +ML_file "Tools/ATP/atp_systems.ML" setup ATP_Systems.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Algebra/Ring.thy --- a/src/HOL/Algebra/Ring.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Algebra/Ring.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,7 +5,6 @@ theory Ring imports FiniteProduct -uses ("ringsimp.ML") begin section {* The Algebraic Hierarchy of Rings *} @@ -389,7 +388,7 @@ text {* Setup algebra method: compute distributive normal form in locale contexts *} -use "ringsimp.ML" +ML_file "ringsimp.ML" setup Algebra.attrib_setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Boogie/Boogie.thy --- a/src/HOL/Boogie/Boogie.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Boogie/Boogie.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,11 +8,6 @@ imports Word keywords "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag -uses - ("Tools/boogie_vcs.ML") - ("Tools/boogie_loader.ML") - ("Tools/boogie_tactics.ML") - ("Tools/boogie_commands.ML") begin text {* @@ -95,12 +90,12 @@ *} setup Boogie_Axioms.setup -use "Tools/boogie_vcs.ML" -use "Tools/boogie_loader.ML" -use "Tools/boogie_tactics.ML" +ML_file "Tools/boogie_vcs.ML" +ML_file "Tools/boogie_loader.ML" +ML_file "Tools/boogie_tactics.ML" setup Boogie_Tactics.setup -use "Tools/boogie_commands.ML" +ML_file "Tools/boogie_commands.ML" setup Boogie_Commands.setup end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Code_Evaluation.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Code_Evaluation imports Plain Typerep Code_Numeral Predicate -uses ("Tools/code_evaluation.ML") begin subsection {* Term representation *} @@ -73,7 +72,7 @@ shows "x \ y" using assms by simp -use "Tools/code_evaluation.ML" +ML_file "Tools/code_evaluation.ML" code_reserved Eval Code_Evaluation diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Datatype.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,10 +8,6 @@ theory Datatype imports Product_Type Sum_Type Nat keywords "datatype" :: thy_decl -uses - ("Tools/Datatype/datatype.ML") - ("Tools/inductive_realizer.ML") - ("Tools/Datatype/datatype_realizer.ML") begin subsection {* The datatype universe *} @@ -517,12 +513,12 @@ hide_type (open) node item hide_const (open) Push Node Atom Leaf Numb Lim Split Case -use "Tools/Datatype/datatype.ML" +ML_file "Tools/Datatype/datatype.ML" -use "Tools/inductive_realizer.ML" +ML_file "Tools/inductive_realizer.ML" setup InductiveRealizer.setup -use "Tools/Datatype/datatype_realizer.ML" +ML_file "Tools/Datatype/datatype_realizer.ML" setup Datatype_Realizer.setup end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Decision_Procs/Commutative_Ring.thy --- a/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Commutative_Ring imports Main Parity -uses ("commutative_ring_tac.ML") begin text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *} @@ -313,7 +312,7 @@ qed -use "commutative_ring_tac.ML" +ML_file "commutative_ring_tac.ML" method_setup comm_ring = {* Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,7 +4,6 @@ theory Cooper imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" -uses ("cooper_tac.ML") begin (* Periodicity of dvd *) @@ -2004,7 +2003,7 @@ end; *} -use "cooper_tac.ML" +ML_file "cooper_tac.ML" method_setup cooper = {* Args.mode "no_quantify" >> diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,13 +7,11 @@ theory Dense_Linear_Order imports Main -uses - "langford_data.ML" - "ferrante_rackoff_data.ML" - ("langford.ML") - ("ferrante_rackoff.ML") begin +ML_file "langford_data.ML" +ML_file "ferrante_rackoff_data.ML" + setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *} context linorder @@ -290,7 +288,7 @@ lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib -use "langford.ML" +ML_file "langford.ML" method_setup dlo = {* Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac) *} "Langford's algorithm for quantifier elimination in dense linear orders" @@ -540,7 +538,7 @@ end -use "ferrante_rackoff.ML" +ML_file "ferrante_rackoff.ML" method_setup ferrack = {* Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,7 +5,6 @@ theory Ferrack imports Complex_Main Dense_Linear_Order DP_Library "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" -uses ("ferrack_tac.ML") begin section {* Quantifier elimination for @{text "\ (0, 1, +, <)"} *} @@ -2003,7 +2002,7 @@ end; *} -use "ferrack_tac.ML" +ML_file "ferrack_tac.ML" method_setup rferrack = {* Args.mode "no_quantify" >> diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Decision_Procs/MIR.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,7 +5,6 @@ theory MIR imports Complex_Main Dense_Linear_Order DP_Library "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef" -uses ("mir_tac.ML") begin section {* Quantifier elimination for @{text "\ (0, 1, +, floor, <)"} *} @@ -5634,7 +5633,7 @@ end; *} -use "mir_tac.ML" +ML_file "mir_tac.ML" method_setup mir = {* Args.mode "no_quantify" >> diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Divides.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,10 @@ theory Divides imports Nat_Transfer -uses "~~/src/Provers/Arith/cancel_div_mod.ML" begin +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" + subsection {* Syntactic division operations *} class div = dvd + diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Extraction.thy --- a/src/HOL/Extraction.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Extraction.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory Extraction imports Option -uses "Tools/rewrite_hol_proof.ML" begin +ML_file "Tools/rewrite_hol_proof.ML" + subsection {* Setup *} setup {* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Finite_Set.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Finite_Set imports Option Power -uses ("Tools/set_comprehension_pointfree.ML") begin subsection {* Predicate for finite sets *} @@ -18,7 +17,7 @@ | insertI [simp, intro!]: "finite A \ finite (insert a A)" (* FIXME: move to Set theory *) -use "Tools/set_comprehension_pointfree.ML" +ML_file "Tools/set_comprehension_pointfree.ML" simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Fun.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,7 +8,6 @@ theory Fun imports Complete_Lattices keywords "enriched_type" :: thy_goal -uses ("Tools/enriched_type.ML") begin lemma apply_inverse: @@ -801,7 +800,7 @@ subsubsection {* Functorial structure of types *} -use "Tools/enriched_type.ML" +ML_file "Tools/enriched_type.ML" enriched_type map_fun: map_fun by (simp_all add: fun_eq_iff) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/FunDef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,27 +7,11 @@ theory FunDef imports Partial_Function Wellfounded keywords "function" "termination" :: thy_goal and "fun" :: thy_decl -uses - "Tools/prop_logic.ML" - "Tools/sat_solver.ML" - ("Tools/Function/function_common.ML") - ("Tools/Function/context_tree.ML") - ("Tools/Function/function_core.ML") - ("Tools/Function/sum_tree.ML") - ("Tools/Function/mutual.ML") - ("Tools/Function/pattern_split.ML") - ("Tools/Function/function.ML") - ("Tools/Function/relation.ML") - ("Tools/Function/measure_functions.ML") - ("Tools/Function/lexicographic_order.ML") - ("Tools/Function/pat_completeness.ML") - ("Tools/Function/fun.ML") - ("Tools/Function/induction_schema.ML") - ("Tools/Function/termination.ML") - ("Tools/Function/scnp_solve.ML") - ("Tools/Function/scnp_reconstruct.ML") begin +ML_file "Tools/prop_logic.ML" +ML_file "Tools/sat_solver.ML" + subsection {* Definitions with default value. *} definition @@ -101,27 +85,27 @@ "wf R \ wfP (in_rel R)" by (simp add: wfP_def) -use "Tools/Function/function_common.ML" -use "Tools/Function/context_tree.ML" -use "Tools/Function/function_core.ML" -use "Tools/Function/sum_tree.ML" -use "Tools/Function/mutual.ML" -use "Tools/Function/pattern_split.ML" -use "Tools/Function/relation.ML" +ML_file "Tools/Function/function_common.ML" +ML_file "Tools/Function/context_tree.ML" +ML_file "Tools/Function/function_core.ML" +ML_file "Tools/Function/sum_tree.ML" +ML_file "Tools/Function/mutual.ML" +ML_file "Tools/Function/pattern_split.ML" +ML_file "Tools/Function/relation.ML" method_setup relation = {* Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t)) *} "prove termination using a user-specified wellfounded relation" -use "Tools/Function/function.ML" -use "Tools/Function/pat_completeness.ML" +ML_file "Tools/Function/function.ML" +ML_file "Tools/Function/pat_completeness.ML" method_setup pat_completeness = {* Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac) *} "prove completeness of datatype patterns" -use "Tools/Function/fun.ML" -use "Tools/Function/induction_schema.ML" +ML_file "Tools/Function/fun.ML" +ML_file "Tools/Function/induction_schema.ML" method_setup induction_schema = {* Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac) @@ -137,7 +121,7 @@ inductive is_measure :: "('a \ nat) \ bool" where is_measure_trivial: "is_measure f" -use "Tools/Function/measure_functions.ML" +ML_file "Tools/Function/measure_functions.ML" setup MeasureFunctions.setup lemma measure_size[measure_function]: "is_measure size" @@ -148,7 +132,7 @@ lemma measure_snd[measure_function]: "is_measure f \ is_measure (\p. f (snd p))" by (rule is_measure_trivial) -use "Tools/Function/lexicographic_order.ML" +ML_file "Tools/Function/lexicographic_order.ML" method_setup lexicographic_order = {* Method.sections clasimp_modifiers >> @@ -323,9 +307,9 @@ subsection {* Tool setup *} -use "Tools/Function/termination.ML" -use "Tools/Function/scnp_solve.ML" -use "Tools/Function/scnp_reconstruct.ML" +ML_file "Tools/Function/termination.ML" +ML_file "Tools/Function/scnp_solve.ML" +ML_file "Tools/Function/scnp_reconstruct.ML" setup {* ScnpReconstruct.setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Groebner_Basis.thy --- a/src/HOL/Groebner_Basis.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Groebner_Basis.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,8 +6,6 @@ theory Groebner_Basis imports Semiring_Normalization -uses - ("Tools/groebner.ML") begin subsection {* Groebner Bases *} @@ -41,7 +39,7 @@ setup Algebra_Simplification.setup -use "Tools/groebner.ML" +ML_file "Tools/groebner.ML" method_setup algebra = {* let diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Groups.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Groups imports Orderings -uses ("Tools/group_cancel.ML") begin subsection {* Fact collections *} @@ -830,7 +829,7 @@ end -use "Tools/group_cancel.ML" +ML_file "Tools/group_cancel.ML" simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOL.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,37 +10,32 @@ "try" "solve_direct" "quickcheck" "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and "quickcheck_params" :: thy_decl -uses - ("Tools/hologic.ML") - "~~/src/Tools/misc_legacy.ML" - "~~/src/Tools/try.ML" - "~~/src/Tools/quickcheck.ML" - "~~/src/Tools/solve_direct.ML" - "~~/src/Tools/IsaPlanner/zipper.ML" - "~~/src/Tools/IsaPlanner/isand.ML" - "~~/src/Tools/IsaPlanner/rw_tools.ML" - "~~/src/Tools/IsaPlanner/rw_inst.ML" - "~~/src/Provers/hypsubst.ML" - "~~/src/Provers/splitter.ML" - "~~/src/Provers/classical.ML" - "~~/src/Provers/blast.ML" - "~~/src/Provers/clasimp.ML" - "~~/src/Tools/coherent.ML" - "~~/src/Tools/eqsubst.ML" - "~~/src/Provers/quantifier1.ML" - ("Tools/simpdata.ML") - "~~/src/Tools/atomize_elim.ML" - "~~/src/Tools/induct.ML" - "~~/src/Tools/cong_tac.ML" - "~~/src/Tools/intuitionistic.ML" - "~~/src/Tools/project_rule.ML" - ("~~/src/Tools/induction.ML") - ("~~/src/Tools/induct_tacs.ML") - ("Tools/cnf_funcs.ML") - "~~/src/Tools/subtyping.ML" - "~~/src/Tools/case_product.ML" begin +ML_file "~~/src/Tools/misc_legacy.ML" +ML_file "~~/src/Tools/try.ML" +ML_file "~~/src/Tools/quickcheck.ML" +ML_file "~~/src/Tools/solve_direct.ML" +ML_file "~~/src/Tools/IsaPlanner/zipper.ML" +ML_file "~~/src/Tools/IsaPlanner/isand.ML" +ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML" +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" +ML_file "~~/src/Provers/hypsubst.ML" +ML_file "~~/src/Provers/splitter.ML" +ML_file "~~/src/Provers/classical.ML" +ML_file "~~/src/Provers/blast.ML" +ML_file "~~/src/Provers/clasimp.ML" +ML_file "~~/src/Tools/coherent.ML" +ML_file "~~/src/Tools/eqsubst.ML" +ML_file "~~/src/Provers/quantifier1.ML" +ML_file "~~/src/Tools/atomize_elim.ML" +ML_file "~~/src/Tools/induct.ML" +ML_file "~~/src/Tools/cong_tac.ML" +ML_file "~~/src/Tools/intuitionistic.ML" +ML_file "~~/src/Tools/project_rule.ML" +ML_file "~~/src/Tools/subtyping.ML" +ML_file "~~/src/Tools/case_product.ML" + setup {* Intuitionistic.method_setup @{binding iprover} #> Quickcheck.setup @@ -702,7 +697,7 @@ and [sym] = sym not_sym and [Pure.elim?] = iffD1 iffD2 impE -use "Tools/hologic.ML" +ML_file "Tools/hologic.ML" subsubsection {* Atomizing meta-level connectives *} @@ -1193,7 +1188,7 @@ "(\x y. P x y) = (\y x. P x y)" by blast -use "Tools/simpdata.ML" +ML_file "Tools/simpdata.ML" ML {* open Simpdata *} setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *} @@ -1481,7 +1476,7 @@ ) *} -use "~~/src/Tools/induction.ML" +ML_file "~~/src/Tools/induction.ML" setup {* Induct.setup #> Induction.setup #> @@ -1563,7 +1558,7 @@ hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false -use "~~/src/Tools/induct_tacs.ML" +ML_file "~~/src/Tools/induct_tacs.ML" setup Induct_Tacs.setup @@ -1701,7 +1696,7 @@ val trans = @{thm trans} *} -use "Tools/cnf_funcs.ML" +ML_file "Tools/cnf_funcs.ML" subsection {* Code generator setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOLCF/Cpodef.thy --- a/src/HOL/HOLCF/Cpodef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOLCF/Cpodef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Cpodef imports Adm keywords "pcpodef" "cpodef" :: thy_goal -uses ("Tools/cpodef.ML") begin subsection {* Proving a subtype is a partial order *} @@ -268,6 +267,6 @@ subsection {* HOLCF type definition package *} -use "Tools/cpodef.ML" +ML_file "Tools/cpodef.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOLCF/Domain.thy --- a/src/HOL/HOLCF/Domain.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOLCF/Domain.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,11 +9,6 @@ keywords "domaindef" :: thy_decl and "lazy" "unsafe" and "domain_isomorphism" "domain" :: thy_decl -uses - ("Tools/domaindef.ML") - ("Tools/Domain/domain_isomorphism.ML") - ("Tools/Domain/domain_axioms.ML") - ("Tools/Domain/domain.ML") begin default_sort "domain" @@ -155,7 +150,7 @@ , (@{const_name liftprj}, SOME @{typ "udom u \ 'a::predomain u"}) ] *} -use "Tools/domaindef.ML" +ML_file "Tools/domaindef.ML" subsection {* Isomorphic deflations *} @@ -321,9 +316,9 @@ subsection {* Setting up the domain package *} -use "Tools/Domain/domain_isomorphism.ML" -use "Tools/Domain/domain_axioms.ML" -use "Tools/Domain/domain.ML" +ML_file "Tools/Domain/domain_isomorphism.ML" +ML_file "Tools/Domain/domain_axioms.ML" +ML_file "Tools/Domain/domain.ML" setup Domain_Isomorphism.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOLCF/Domain_Aux.thy --- a/src/HOL/HOLCF/Domain_Aux.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOLCF/Domain_Aux.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,12 +6,6 @@ theory Domain_Aux imports Map_Functions Fixrec -uses - ("Tools/Domain/domain_take_proofs.ML") - ("Tools/cont_consts.ML") - ("Tools/cont_proc.ML") - ("Tools/Domain/domain_constructors.ML") - ("Tools/Domain/domain_induction.ML") begin subsection {* Continuous isomorphisms *} @@ -350,11 +344,11 @@ subsection {* ML setup *} -use "Tools/Domain/domain_take_proofs.ML" -use "Tools/cont_consts.ML" -use "Tools/cont_proc.ML" -use "Tools/Domain/domain_constructors.ML" -use "Tools/Domain/domain_induction.ML" +ML_file "Tools/Domain/domain_take_proofs.ML" +ML_file "Tools/cont_consts.ML" +ML_file "Tools/cont_proc.ML" +ML_file "Tools/Domain/domain_constructors.ML" +ML_file "Tools/Domain/domain_induction.ML" setup Domain_Take_Proofs.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOLCF/Fixrec.thy --- a/src/HOL/HOLCF/Fixrec.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOLCF/Fixrec.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,6 @@ theory Fixrec imports Plain_HOLCF keywords "fixrec" :: thy_decl -uses - ("Tools/holcf_library.ML") - ("Tools/fixrec.ML") begin subsection {* Pattern-match monad *} @@ -227,8 +224,8 @@ subsection {* Initializing the fixrec package *} -use "Tools/holcf_library.ML" -use "Tools/fixrec.ML" +ML_file "Tools/holcf_library.ML" +ML_file "Tools/fixrec.ML" method_setup fixrec_simp = {* Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory Correctness imports IOA Env Impl Impl_finite -uses "Check.ML" begin +ML_file "Check.ML" + primrec reduce :: "'a list => 'a list" where reduce_Nil: "reduce [] = []" diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Hilbert_Choice.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,7 +8,6 @@ theory Hilbert_Choice imports Nat Wellfounded Plain keywords "specification" "ax_specification" :: thy_goal -uses ("Tools/choice_specification.ML") begin subsection {* Hilbert's epsilon *} @@ -649,6 +648,6 @@ lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c" by (simp only: someI_ex) -use "Tools/choice_specification.ML" +ML_file "Tools/choice_specification.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Hoare/Hoare_Logic.thy --- a/src/HOL/Hoare/Hoare_Logic.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,7 +10,6 @@ theory Hoare_Logic imports Main -uses ("hoare_syntax.ML") ("hoare_tac.ML") begin type_synonym 'a bexp = "'a set" @@ -54,7 +53,7 @@ "_hoare" :: "['a assn,'a com,'a assn] => bool" ("{_} // _ // {_}" [0,55,0] 50) -use "hoare_syntax.ML" +ML_file "hoare_syntax.ML" parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *} print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *} @@ -94,7 +93,7 @@ by blast lemmas AbortRule = SkipRule -- "dummy version" -use "hoare_tac.ML" +ML_file "hoare_tac.ML" method_setup vcg = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Hoare/Hoare_Logic_Abort.thy --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Hoare_Logic_Abort imports Main -uses ("hoare_syntax.ML") ("hoare_tac.ML") begin type_synonym 'a bexp = "'a set" @@ -56,7 +55,7 @@ "_hoare_abort" :: "['a assn,'a com,'a assn] => bool" ("{_} // _ // {_}" [0,55,0] 50) -use "hoare_syntax.ML" +ML_file "hoare_syntax.ML" parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *} print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *} @@ -105,7 +104,7 @@ lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" by blast -use "hoare_tac.ML" +ML_file "hoare_tac.ML" method_setup vcg = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Import/Import_Setup.thy --- a/src/HOL/Import/Import_Setup.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Import/Import_Setup.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,12 +7,11 @@ theory Import_Setup imports "~~/src/HOL/Parity" "~~/src/HOL/Fact" -keywords - "import_type_map" :: thy_decl and "import_const_map" :: thy_decl and - "import_file" :: thy_decl -uses "import_data.ML" ("import_rule.ML") +keywords "import_type_map" "import_const_map" "import_file" :: thy_decl begin +ML_file "import_data.ML" + lemma light_ex_imp_nonempty: "P t \ \x. x \ Collect P" by auto @@ -27,7 +26,7 @@ "(\x. f x = g x) \ f = g" by auto -use "import_rule.ML" +ML_file "import_rule.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Inductive.thy Wed Aug 22 22:55:41 2012 +0200 @@ -11,15 +11,6 @@ "inductive_cases" "inductive_simps" :: thy_script and "monos" and "rep_datatype" :: thy_goal and "primrec" :: thy_decl -uses - ("Tools/inductive.ML") - ("Tools/Datatype/datatype_aux.ML") - ("Tools/Datatype/datatype_prop.ML") - ("Tools/Datatype/datatype_data.ML") - ("Tools/Datatype/datatype_case.ML") - ("Tools/Datatype/rep_datatype.ML") - ("Tools/Datatype/datatype_codegen.ML") - ("Tools/Datatype/primrec.ML") begin subsection {* Least and greatest fixed points *} @@ -264,7 +255,7 @@ subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj Collect_mono in_mono vimage_mono -use "Tools/inductive.ML" +ML_file "Tools/inductive.ML" setup Inductive.setup theorems [mono] = @@ -278,13 +269,13 @@ text {* Package setup. *} -use "Tools/Datatype/datatype_aux.ML" -use "Tools/Datatype/datatype_prop.ML" -use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup -use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup -use "Tools/Datatype/rep_datatype.ML" -use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup -use "Tools/Datatype/primrec.ML" +ML_file "Tools/Datatype/datatype_aux.ML" +ML_file "Tools/Datatype/datatype_prop.ML" +ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup +ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup +ML_file "Tools/Datatype/rep_datatype.ML" +ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup +ML_file "Tools/Datatype/primrec.ML" text{* Lambda-abstractions with pattern matching: *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Int.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,8 +7,6 @@ theory Int imports Equiv_Relations Wellfounded Quotient -uses - ("Tools/int_arith.ML") begin subsection {* Definition of integers as a quotient type *} @@ -719,7 +717,7 @@ of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult of_int_0 of_int_1 of_int_add of_int_mult -use "Tools/int_arith.ML" +ML_file "Tools/int_arith.ML" declaration {* K Int_Arith.setup *} simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Isar_Examples/Hoare.thy --- a/src/HOL/Isar_Examples/Hoare.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Isar_Examples/Hoare.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,7 +8,6 @@ theory Hoare imports Main -uses ("~~/src/HOL/Hoare/hoare_tac.ML") begin subsection {* Abstract syntax and semantics *} @@ -402,7 +401,7 @@ lemmas AbortRule = SkipRule -- "dummy version" -use "~~/src/HOL/Hoare/hoare_tac.ML" +ML_file "~~/src/HOL/Hoare/hoare_tac.ML" method_setup hoare = {* Scan.succeed (fn ctxt => diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Library/Code_Prolog.thy --- a/src/HOL/Library/Code_Prolog.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Library/Code_Prolog.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory Code_Prolog imports Main -uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" begin +ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML" + section {* Setup for Numerals *} setup {* Predicate_Compile_Data.ignore_consts diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Library/Old_Recdef.thy --- a/src/HOL/Library/Old_Recdef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Library/Old_Recdef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,17 +10,6 @@ "recdef" "defer_recdef" :: thy_decl and "recdef_tc" :: thy_goal and "permissive" "congs" "hints" -uses - ("~~/src/HOL/Tools/TFL/casesplit.ML") - ("~~/src/HOL/Tools/TFL/utils.ML") - ("~~/src/HOL/Tools/TFL/usyntax.ML") - ("~~/src/HOL/Tools/TFL/dcterm.ML") - ("~~/src/HOL/Tools/TFL/thms.ML") - ("~~/src/HOL/Tools/TFL/rules.ML") - ("~~/src/HOL/Tools/TFL/thry.ML") - ("~~/src/HOL/Tools/TFL/tfl.ML") - ("~~/src/HOL/Tools/TFL/post.ML") - ("~~/src/HOL/Tools/recdef.ML") begin subsection {* Lemmas for TFL *} @@ -66,16 +55,16 @@ lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" by blast -use "~~/src/HOL/Tools/TFL/casesplit.ML" -use "~~/src/HOL/Tools/TFL/utils.ML" -use "~~/src/HOL/Tools/TFL/usyntax.ML" -use "~~/src/HOL/Tools/TFL/dcterm.ML" -use "~~/src/HOL/Tools/TFL/thms.ML" -use "~~/src/HOL/Tools/TFL/rules.ML" -use "~~/src/HOL/Tools/TFL/thry.ML" -use "~~/src/HOL/Tools/TFL/tfl.ML" -use "~~/src/HOL/Tools/TFL/post.ML" -use "~~/src/HOL/Tools/recdef.ML" +ML_file "~~/src/HOL/Tools/TFL/casesplit.ML" +ML_file "~~/src/HOL/Tools/TFL/utils.ML" +ML_file "~~/src/HOL/Tools/TFL/usyntax.ML" +ML_file "~~/src/HOL/Tools/TFL/dcterm.ML" +ML_file "~~/src/HOL/Tools/TFL/thms.ML" +ML_file "~~/src/HOL/Tools/TFL/rules.ML" +ML_file "~~/src/HOL/Tools/TFL/thry.ML" +ML_file "~~/src/HOL/Tools/TFL/tfl.ML" +ML_file "~~/src/HOL/Tools/TFL/post.ML" +ML_file "~~/src/HOL/Tools/recdef.ML" setup Recdef.setup subsection {* Rule setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Library/Predicate_Compile_Quickcheck.thy --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,9 +4,10 @@ theory Predicate_Compile_Quickcheck imports Main Predicate_Compile_Alternative_Defs -uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" begin +ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" + setup {* Predicate_Compile_Quickcheck.setup *} end \ No newline at end of file diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Library/Reflection.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,11 +6,11 @@ theory Reflection imports Main -uses - "~~/src/HOL/Library/reify_data.ML" - "~~/src/HOL/Library/reflection.ML" begin +ML_file "~~/src/HOL/Library/reify_data.ML" +ML_file "~~/src/HOL/Library/reflection.ML" + setup {* Reify_Data.setup *} method_setup reify = {* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Library/Sum_of_Squares.thy --- a/src/HOL/Library/Sum_of_Squares.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Library/Sum_of_Squares.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,13 +8,13 @@ theory Sum_of_Squares imports Complex_Main -uses - "positivstellensatz.ML" - "Sum_of_Squares/sum_of_squares.ML" - "Sum_of_Squares/positivstellensatz_tools.ML" - "Sum_of_Squares/sos_wrapper.ML" begin +ML_file "positivstellensatz.ML" +ML_file "Sum_of_Squares/sum_of_squares.ML" +ML_file "Sum_of_Squares/positivstellensatz_tools.ML" +ML_file "Sum_of_Squares/sos_wrapper.ML" + text {* Proof method sos invocations: \begin{itemize} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Lifting.thy Wed Aug 22 22:55:41 2012 +0200 @@ -11,12 +11,6 @@ "print_quotmaps" "print_quotients" :: diag and "lift_definition" :: thy_goal and "setup_lifting" :: thy_decl -uses - ("Tools/Lifting/lifting_util.ML") - ("Tools/Lifting/lifting_info.ML") - ("Tools/Lifting/lifting_term.ML") - ("Tools/Lifting/lifting_def.ML") - ("Tools/Lifting/lifting_setup.ML") begin subsection {* Function map *} @@ -418,19 +412,19 @@ subsection {* ML setup *} -use "Tools/Lifting/lifting_util.ML" +ML_file "Tools/Lifting/lifting_util.ML" -use "Tools/Lifting/lifting_info.ML" +ML_file "Tools/Lifting/lifting_info.ML" setup Lifting_Info.setup declare fun_quotient[quot_map] lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition -use "Tools/Lifting/lifting_term.ML" +ML_file "Tools/Lifting/lifting_term.ML" -use "Tools/Lifting/lifting_def.ML" +ML_file "Tools/Lifting/lifting_def.ML" -use "Tools/Lifting/lifting_setup.ML" +ML_file "Tools/Lifting/lifting_setup.ML" hide_const (open) invariant diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/List.thy --- a/src/HOL/List.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/List.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,6 @@ theory List imports Plain Presburger Code_Numeral Quotient ATP -uses - ("Tools/list_code.ML") - ("Tools/list_to_set_comprehension.ML") begin datatype 'a list = @@ -485,7 +482,7 @@ *) -use "Tools/list_to_set_comprehension.ML" +ML_file "Tools/list_to_set_comprehension.ML" simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *} @@ -5522,7 +5519,7 @@ subsubsection {* Pretty lists *} -use "Tools/list_code.ML" +ML_file "Tools/list_code.ML" code_type list (SML "_ list") diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Matrix_LP/ComputeFloat.thy --- a/src/HOL/Matrix_LP/ComputeFloat.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory ComputeFloat imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" -uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML") begin +ML_file "~~/src/Tools/float.ML" + definition int_of_real :: "real \ int" where "int_of_real x = (SOME y. real y = x)" @@ -238,6 +239,6 @@ lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0 nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false -use "~~/src/HOL/Tools/float_arith.ML" +ML_file "~~/src/HOL/Tools/float_arith.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy --- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,7 +5,15 @@ *) theory Compute_Oracle imports HOL -uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML" begin +ML_file "am.ML" +ML_file "am_compiler.ML" +ML_file "am_interpreter.ML" +ML_file "am_ghc.ML" +ML_file "am_sml.ML" +ML_file "report.ML" +ML_file "compute.ML" +ML_file "linker.ML" + end \ No newline at end of file diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Matrix_LP/Cplex.thy --- a/src/HOL/Matrix_LP/Cplex.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Matrix_LP/Cplex.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,10 +4,13 @@ theory Cplex imports SparseMatrix LP ComputeFloat ComputeNumeral -uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" - "fspmlp.ML" ("matrixlp.ML") begin +ML_file "Cplex_tools.ML" +ML_file "CplexMatrixConverter.ML" +ML_file "FloatSparseMatrixBuilder.ML" +ML_file "fspmlp.ML" + lemma spm_mult_le_dual_prts: assumes "sorted_sparse_matrix A1" @@ -61,7 +64,7 @@ (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))" by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def]) -use "matrixlp.ML" +ML_file "matrixlp.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Meson.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,9 +9,6 @@ theory Meson imports Datatype -uses ("Tools/Meson/meson.ML") - ("Tools/Meson/meson_clausify.ML") - ("Tools/Meson/meson_tactic.ML") begin subsection {* Negation Normal Form *} @@ -194,9 +191,9 @@ subsection {* Meson package *} -use "Tools/Meson/meson.ML" -use "Tools/Meson/meson_clausify.ML" -use "Tools/Meson/meson_tactic.ML" +ML_file "Tools/Meson/meson.ML" +ML_file "Tools/Meson/meson_clausify.ML" +ML_file "Tools/Meson/meson_tactic.ML" setup {* Meson_Tactic.setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Metis.thy --- a/src/HOL/Metis.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Metis.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,13 +9,10 @@ theory Metis imports ATP keywords "try0" :: diag -uses "~~/src/Tools/Metis/metis.ML" - ("Tools/Metis/metis_generate.ML") - ("Tools/Metis/metis_reconstruct.ML") - ("Tools/Metis/metis_tactic.ML") - ("Tools/try0.ML") begin +ML_file "~~/src/Tools/Metis/metis.ML" + subsection {* Literal selection and lambda-lifting helpers *} definition select :: "'a \ 'a" where @@ -41,9 +38,9 @@ subsection {* Metis package *} -use "Tools/Metis/metis_generate.ML" -use "Tools/Metis/metis_reconstruct.ML" -use "Tools/Metis/metis_tactic.ML" +ML_file "Tools/Metis/metis_generate.ML" +ML_file "Tools/Metis/metis_reconstruct.ML" +ML_file "Tools/Metis/metis_tactic.ML" setup {* Metis_Tactic.setup *} @@ -58,8 +55,7 @@ subsection {* Try0 *} -use "Tools/try0.ML" - +ML_file "Tools/try0.ML" setup {* Try0.setup *} end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,10 +4,11 @@ theory Mirabelle imports Sledgehammer -uses "Tools/mirabelle.ML" - "../TPTP/sledgehammer_tactics.ML" begin +ML_file "Tools/mirabelle.ML" +ML_file "../TPTP/sledgehammer_tactics.ML" + (* no multithreading, no parallel proofs *) (* FIXME *) ML {* Multithreading.max_threads := 1 *} ML {* Goal.parallel_proofs := 0 *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Mirabelle/Mirabelle_Test.thy --- a/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,16 +6,16 @@ theory Mirabelle_Test imports Main Mirabelle -uses - "Tools/mirabelle_arith.ML" - "Tools/mirabelle_metis.ML" - "Tools/mirabelle_quickcheck.ML" - "Tools/mirabelle_refute.ML" - "Tools/mirabelle_sledgehammer.ML" - "Tools/mirabelle_sledgehammer_filter.ML" - "Tools/mirabelle_try0.ML" begin +ML_file "Tools/mirabelle_arith.ML" +ML_file "Tools/mirabelle_metis.ML" +ML_file "Tools/mirabelle_quickcheck.ML" +ML_file "Tools/mirabelle_refute.ML" +ML_file "Tools/mirabelle_sledgehammer.ML" +ML_file "Tools/mirabelle_sledgehammer_filter.ML" +ML_file "Tools/mirabelle_try0.ML" + text {* Only perform type-checking of the actions, any reasonable test would be too complicated. diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Multivariate_Analysis/Norm_Arith.thy --- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Norm_Arith imports "~~/src/HOL/Library/Sum_of_Squares" -uses ("normarith.ML") begin lemma norm_cmul_rule_thm: @@ -111,7 +110,7 @@ mult_1_left mult_1_right -use "normarith.ML" +ML_file "normarith.ML" method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) *} "prove simple linear statements about vector norms" diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Mutabelle/Mutabelle.thy --- a/src/HOL/Mutabelle/Mutabelle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Mutabelle/Mutabelle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -2,9 +2,10 @@ theory Mutabelle imports Main -uses "mutabelle.ML" begin +ML_file "mutabelle.ML" + ML {* val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]; diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Mutabelle/MutabelleExtra.thy --- a/src/HOL/Mutabelle/MutabelleExtra.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,11 +9,11 @@ "~/repos/afp/thys/Polynomials/Polynomial" "~/repos/afp/thys/Presburger-Automata/Presburger_Automata" "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*) -uses - "mutabelle.ML" - "mutabelle_extra.ML" begin +ML_file "mutabelle.ML" +ML_file "mutabelle_extra.ML" + section {* configuration *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/NSA/StarDef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory StarDef imports Filter -uses ("transfer.ML") begin subsection {* A Free Ultrafilter over the Naturals *} @@ -88,7 +87,7 @@ by (subgoal_tac "P \ Q", simp, simp add: atomize_eq) text {*Initialize transfer tactic.*} -use "transfer.ML" +ML_file "transfer.ML" setup Transfer_Principle.setup method_setup transfer = {* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Nat.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,14 +9,13 @@ theory Nat imports Inductive Typedef Fun Fields -uses - "~~/src/Tools/rat.ML" - "Tools/arith_data.ML" - ("Tools/nat_arith.ML") - "~~/src/Provers/Arith/fast_lin_arith.ML" - ("Tools/lin_arith.ML") begin +ML_file "~~/src/Tools/rat.ML" +ML_file "Tools/arith_data.ML" +ML_file "~~/src/Provers/Arith/fast_lin_arith.ML" + + subsection {* Type @{text ind} *} typedecl ind @@ -1492,7 +1491,7 @@ setup Arith_Data.setup -use "Tools/nat_arith.ML" +ML_file "Tools/nat_arith.ML" simproc_setup nateq_cancel_sums ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") = @@ -1510,7 +1509,7 @@ ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *} -use "Tools/lin_arith.ML" +ML_file "Tools/lin_arith.ML" setup {* Lin_Arith.global_setup *} declaration {* K Lin_Arith.setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Nat_Transfer.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,7 +5,6 @@ theory Nat_Transfer imports Int -uses ("Tools/legacy_transfer.ML") begin subsection {* Generic transfer machinery *} @@ -16,8 +15,7 @@ lemma transfer_morphismI[intro]: "transfer_morphism f A" by (simp add: transfer_morphism_def) -use "Tools/legacy_transfer.ML" - +ML_file "Tools/legacy_transfer.ML" setup Legacy_Transfer.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Nitpick.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,21 +10,6 @@ theory Nitpick imports Map Quotient SAT Record keywords "nitpick" :: diag and "nitpick_params" :: thy_decl -uses ("Tools/Nitpick/kodkod.ML") - ("Tools/Nitpick/kodkod_sat.ML") - ("Tools/Nitpick/nitpick_util.ML") - ("Tools/Nitpick/nitpick_hol.ML") - ("Tools/Nitpick/nitpick_preproc.ML") - ("Tools/Nitpick/nitpick_mono.ML") - ("Tools/Nitpick/nitpick_scope.ML") - ("Tools/Nitpick/nitpick_peephole.ML") - ("Tools/Nitpick/nitpick_rep.ML") - ("Tools/Nitpick/nitpick_nut.ML") - ("Tools/Nitpick/nitpick_kodkod.ML") - ("Tools/Nitpick/nitpick_model.ML") - ("Tools/Nitpick/nitpick.ML") - ("Tools/Nitpick/nitpick_isar.ML") - ("Tools/Nitpick/nitpick_tests.ML") begin typedecl bisim_iterator @@ -212,21 +197,21 @@ definition of_frac :: "'a \ 'b\{inverse,ring_1}" where "of_frac q \ of_int (num q) / of_int (denom q)" -use "Tools/Nitpick/kodkod.ML" -use "Tools/Nitpick/kodkod_sat.ML" -use "Tools/Nitpick/nitpick_util.ML" -use "Tools/Nitpick/nitpick_hol.ML" -use "Tools/Nitpick/nitpick_mono.ML" -use "Tools/Nitpick/nitpick_preproc.ML" -use "Tools/Nitpick/nitpick_scope.ML" -use "Tools/Nitpick/nitpick_peephole.ML" -use "Tools/Nitpick/nitpick_rep.ML" -use "Tools/Nitpick/nitpick_nut.ML" -use "Tools/Nitpick/nitpick_kodkod.ML" -use "Tools/Nitpick/nitpick_model.ML" -use "Tools/Nitpick/nitpick.ML" -use "Tools/Nitpick/nitpick_isar.ML" -use "Tools/Nitpick/nitpick_tests.ML" +ML_file "Tools/Nitpick/kodkod.ML" +ML_file "Tools/Nitpick/kodkod_sat.ML" +ML_file "Tools/Nitpick/nitpick_util.ML" +ML_file "Tools/Nitpick/nitpick_hol.ML" +ML_file "Tools/Nitpick/nitpick_mono.ML" +ML_file "Tools/Nitpick/nitpick_preproc.ML" +ML_file "Tools/Nitpick/nitpick_scope.ML" +ML_file "Tools/Nitpick/nitpick_peephole.ML" +ML_file "Tools/Nitpick/nitpick_rep.ML" +ML_file "Tools/Nitpick/nitpick_nut.ML" +ML_file "Tools/Nitpick/nitpick_kodkod.ML" +ML_file "Tools/Nitpick/nitpick_model.ML" +ML_file "Tools/Nitpick/nitpick.ML" +ML_file "Tools/Nitpick/nitpick_isar.ML" +ML_file "Tools/Nitpick/nitpick_tests.ML" setup {* Nitpick_Isar.setup #> diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Nitpick_Examples/Mini_Nits.thy --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,9 +9,10 @@ theory Mini_Nits imports Main -uses "minipick.ML" begin +ML_file "minipick.ML" + nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1] nitpick_params [total_consts = smart] diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Nominal/Nominal.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,16 +4,6 @@ "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and "avoids" -uses - ("nominal_thmdecls.ML") - ("nominal_atoms.ML") - ("nominal_datatype.ML") - ("nominal_induct.ML") - ("nominal_permeq.ML") - ("nominal_fresh_fun.ML") - ("nominal_primrec.ML") - ("nominal_inductive.ML") - ("nominal_inductive2.ML") begin section {* Permutations *} @@ -3562,7 +3552,7 @@ (*******************************************************) (* Setup of the theorem attributes eqvt and eqvt_force *) -use "nominal_thmdecls.ML" +ML_file "nominal_thmdecls.ML" setup "NominalThmDecls.setup" lemmas [eqvt] = @@ -3598,11 +3588,11 @@ (***************************************) (* setup for the individial atom-kinds *) (* and nominal datatypes *) -use "nominal_atoms.ML" +ML_file "nominal_atoms.ML" (************************************************************) (* various tactics for analysing permutations, supports etc *) -use "nominal_permeq.ML" +ML_file "nominal_permeq.ML" method_setup perm_simp = {* NominalPermeq.perm_simp_meth *} @@ -3646,7 +3636,7 @@ (*****************************************************************) (* tactics for generating fresh names and simplifying fresh_funs *) -use "nominal_fresh_fun.ML" +ML_file "nominal_fresh_fun.ML" method_setup generate_fresh = {* setup_generate_fresh *} @@ -3662,20 +3652,20 @@ lemma allE_Nil: assumes "\x. P x" obtains "P []" using assms .. -use "nominal_datatype.ML" +ML_file "nominal_datatype.ML" (******************************************************) (* primitive recursive functions on nominal datatypes *) -use "nominal_primrec.ML" +ML_file "nominal_primrec.ML" (****************************************************) (* inductive definition involving nominal datatypes *) -use "nominal_inductive.ML" -use "nominal_inductive2.ML" +ML_file "nominal_inductive.ML" +ML_file "nominal_inductive2.ML" (*****************************************) (* setup for induction principles method *) -use "nominal_induct.ML" +ML_file "nominal_induct.ML" method_setup nominal_induct = {* NominalInduct.nominal_induct_method *} {* nominal induction *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Num.thy --- a/src/HOL/Num.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Num.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,8 +7,6 @@ theory Num imports Datatype -uses - ("Tools/numeral.ML") begin subsection {* The @{text num} type *} @@ -333,7 +331,7 @@ (@{const_syntax neg_numeral}, num_tr' "-")] end *} -use "Tools/numeral.ML" +ML_file "Tools/numeral.ML" subsection {* Class-specific numeral rules *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Numeral_Simprocs.thy --- a/src/HOL/Numeral_Simprocs.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Numeral_Simprocs.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,16 +4,14 @@ theory Numeral_Simprocs imports Divides -uses - "~~/src/Provers/Arith/assoc_fold.ML" - "~~/src/Provers/Arith/cancel_numerals.ML" - "~~/src/Provers/Arith/combine_numerals.ML" - "~~/src/Provers/Arith/cancel_numeral_factor.ML" - "~~/src/Provers/Arith/extract_common_term.ML" - ("Tools/numeral_simprocs.ML") - ("Tools/nat_numeral_simprocs.ML") begin +ML_file "~~/src/Provers/Arith/assoc_fold.ML" +ML_file "~~/src/Provers/Arith/cancel_numerals.ML" +ML_file "~~/src/Provers/Arith/combine_numerals.ML" +ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML" +ML_file "~~/src/Provers/Arith/extract_common_term.ML" + lemmas semiring_norm = Let_def arith_simps nat_arith rel_simps if_False if_True @@ -100,7 +98,7 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) -use "Tools/numeral_simprocs.ML" +ML_file "Tools/numeral_simprocs.ML" simproc_setup semiring_assoc_fold ("(a::'a::comm_semiring_1_cancel) * b") = @@ -210,7 +208,7 @@ |"(l::'a::field_inverse_zero) / (m * n)") = {* fn phi => Numeral_Simprocs.divide_cancel_factor *} -use "Tools/nat_numeral_simprocs.ML" +ML_file "Tools/nat_numeral_simprocs.ML" simproc_setup nat_combine_numerals ("(i::nat) + j" | "Suc (i + j)") = diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Orderings.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,11 +7,11 @@ theory Orderings imports HOL keywords "print_orders" :: diag -uses - "~~/src/Provers/order.ML" - "~~/src/Provers/quasi.ML" (* FIXME unused? *) begin +ML_file "~~/src/Provers/order.ML" +ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) + subsection {* Syntactic orders *} class ord = diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Partial_Function.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,11 +7,10 @@ theory Partial_Function imports Complete_Partial_Order Option keywords "partial_function" :: thy_decl -uses - "Tools/Function/function_lib.ML" - "Tools/Function/partial_function.ML" begin +ML_file "Tools/Function/function_lib.ML" +ML_file "Tools/Function/partial_function.ML" setup Partial_Function.setup subsection {* Axiomatic setup *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Predicate_Compile.thy --- a/src/HOL/Predicate_Compile.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Predicate_Compile.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,20 +7,20 @@ theory Predicate_Compile imports Predicate New_Random_Sequence Quickcheck_Exhaustive keywords "code_pred" :: thy_goal and "values" :: diag -uses - "Tools/Predicate_Compile/predicate_compile_aux.ML" - "Tools/Predicate_Compile/predicate_compile_compilations.ML" - "Tools/Predicate_Compile/core_data.ML" - "Tools/Predicate_Compile/mode_inference.ML" - "Tools/Predicate_Compile/predicate_compile_proof.ML" - "Tools/Predicate_Compile/predicate_compile_core.ML" - "Tools/Predicate_Compile/predicate_compile_data.ML" - "Tools/Predicate_Compile/predicate_compile_fun.ML" - "Tools/Predicate_Compile/predicate_compile_pred.ML" - "Tools/Predicate_Compile/predicate_compile_specialisation.ML" - "Tools/Predicate_Compile/predicate_compile.ML" begin +ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML" +ML_file "Tools/Predicate_Compile/core_data.ML" +ML_file "Tools/Predicate_Compile/mode_inference.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_core.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_data.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML" +ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML" +ML_file "Tools/Predicate_Compile/predicate_compile.ML" + setup Predicate_Compile.setup end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,8 +1,9 @@ theory Hotel_Example_Small_Generator imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" -uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML" begin +ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML" + declare Let_def[code_pred_inline] lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Presburger.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,12 +6,11 @@ theory Presburger imports Groebner_Basis Set_Interval -uses - "Tools/Qelim/qelim.ML" - "Tools/Qelim/cooper_procedure.ML" - ("Tools/Qelim/cooper.ML") begin +ML_file "Tools/Qelim/qelim.ML" +ML_file "Tools/Qelim/cooper_procedure.ML" + subsection{* The @{text "-\"} and @{text "+\"} Properties *} lemma minf: @@ -386,7 +385,7 @@ "\x = x'; 0 \ x' \ P = P'\ \ (0 \ (x::int) \ P) = (0 \ x' \ P')" by (simp cong: conj_cong) -use "Tools/Qelim/cooper.ML" +ML_file "Tools/Qelim/cooper.ML" setup Cooper.setup method_setup presburger = {* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Product_Type.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,9 +8,6 @@ theory Product_Type imports Typedef Inductive Fun keywords "inductive_set" "coinductive_set" :: thy_decl -uses - ("Tools/split_rule.ML") - ("Tools/inductive_set.ML") begin subsection {* @{typ bool} is a datatype *} @@ -690,7 +687,7 @@ lemma internal_split_conv: "internal_split c (a, b) = c a b" by (simp only: internal_split_def split_conv) -use "Tools/split_rule.ML" +ML_file "Tools/split_rule.ML" setup Split_Rule.setup hide_const internal_split @@ -1122,7 +1119,7 @@ subsection {* Inductively defined sets *} -use "Tools/inductive_set.ML" +ML_file "Tools/inductive_set.ML" setup Inductive_Set.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Prolog/HOHH.thy --- a/src/HOL/Prolog/HOHH.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Prolog/HOHH.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory HOHH imports HOL -uses "prolog.ML" begin +ML_file "prolog.ML" + method_setup ptac = {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *} "basic Lambda Prolog interpreter" diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Quickcheck.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,9 +4,6 @@ theory Quickcheck imports Random Code_Evaluation Enum -uses - ("Tools/Quickcheck/quickcheck_common.ML") - ("Tools/Quickcheck/random_generators.ML") begin notation fcomp (infixl "\>" 60) @@ -182,8 +179,8 @@ subsection {* Deriving random generators for datatypes *} -use "Tools/Quickcheck/quickcheck_common.ML" -use "Tools/Quickcheck/random_generators.ML" +ML_file "Tools/Quickcheck/quickcheck_common.ML" +ML_file "Tools/Quickcheck/random_generators.ML" setup Random_Generators.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,9 +5,6 @@ theory Quickcheck_Exhaustive imports Quickcheck keywords "quickcheck_generator" :: thy_decl -uses - ("Tools/Quickcheck/exhaustive_generators.ML") - ("Tools/Quickcheck/abstract_generators.ML") begin subsection {* basic operations for exhaustive generators *} @@ -577,7 +574,7 @@ notation (output) unknown ("?") -use "Tools/Quickcheck/exhaustive_generators.ML" +ML_file "Tools/Quickcheck/exhaustive_generators.ML" setup {* Exhaustive_Generators.setup *} @@ -585,7 +582,7 @@ subsection {* Defining generators for abstract types *} -use "Tools/Quickcheck/abstract_generators.ML" +ML_file "Tools/Quickcheck/abstract_generators.ML" hide_fact (open) orelse_def no_notation orelse (infixr "orelse" 55) diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,11 +5,9 @@ theory Quickcheck_Narrowing imports Quickcheck_Exhaustive keywords "find_unused_assms" :: diag -uses +uses (* FIXME session files *) ("Tools/Quickcheck/PNF_Narrowing_Engine.hs") ("Tools/Quickcheck/Narrowing_Engine.hs") - ("Tools/Quickcheck/narrowing_generators.ML") - ("Tools/Quickcheck/find_unused_assms.ML") begin subsection {* Counterexample generator *} @@ -340,7 +338,7 @@ subsubsection {* Setting up the counterexample generator *} -use "Tools/Quickcheck/narrowing_generators.ML" +ML_file "Tools/Quickcheck/narrowing_generators.ML" setup {* Narrowing_Generators.setup *} @@ -447,7 +445,7 @@ subsection {* The @{text find_unused_assms} command *} -use "Tools/Quickcheck/find_unused_assms.ML" +ML_file "Tools/Quickcheck/find_unused_assms.ML" subsection {* Closing up *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Quotient.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,12 +10,6 @@ "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and "quotient_type" :: thy_goal and "/" and "quotient_definition" :: thy_goal -uses - ("Tools/Quotient/quotient_info.ML") - ("Tools/Quotient/quotient_type.ML") - ("Tools/Quotient/quotient_def.ML") - ("Tools/Quotient/quotient_term.ML") - ("Tools/Quotient/quotient_tacs.ML") begin text {* @@ -765,7 +759,7 @@ text {* Auxiliary data for the quotient package *} -use "Tools/Quotient/quotient_info.ML" +ML_file "Tools/Quotient/quotient_info.ML" setup Quotient_Info.setup declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]] @@ -787,15 +781,15 @@ vimage_id text {* Translation functions for the lifting process. *} -use "Tools/Quotient/quotient_term.ML" +ML_file "Tools/Quotient/quotient_term.ML" text {* Definitions of the quotient types. *} -use "Tools/Quotient/quotient_type.ML" +ML_file "Tools/Quotient/quotient_type.ML" text {* Definitions for quotient constants. *} -use "Tools/Quotient/quotient_def.ML" +ML_file "Tools/Quotient/quotient_def.ML" text {* @@ -820,7 +814,7 @@ text {* Tactics for proving the lifted theorems *} -use "Tools/Quotient/quotient_tacs.ML" +ML_file "Tools/Quotient/quotient_tacs.ML" subsection {* Methods / Interface *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Rat.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Rat imports GCD Archimedean_Field -uses ("Tools/float_syntax.ML") begin subsection {* Rational numbers as quotient *} @@ -1107,7 +1106,7 @@ syntax "_Float" :: "float_const \ 'a" ("_") -use "Tools/float_syntax.ML" +ML_file "Tools/float_syntax.ML" setup Float_Syntax.setup text{* Test: *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Real.thy --- a/src/HOL/Real.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Real.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,8 +1,8 @@ theory Real imports RComplete RealVector -uses "Tools/SMT/smt_real.ML" begin -setup {* SMT_Real.setup *} +ML_file "Tools/SMT/smt_real.ML" +setup SMT_Real.setup end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Record.thy --- a/src/HOL/Record.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Record.thy Wed Aug 22 22:55:41 2012 +0200 @@ -11,7 +11,6 @@ theory Record imports Plain Quickcheck_Narrowing keywords "record" :: thy_decl -uses ("Tools/record.ML") begin subsection {* Introduction *} @@ -461,7 +460,7 @@ subsection {* Record package *} -use "Tools/record.ML" setup Record.setup +ML_file "Tools/record.ML" setup Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Refute.thy --- a/src/HOL/Refute.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Refute.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,9 +10,9 @@ theory Refute imports Hilbert_Choice List Sledgehammer keywords "refute" :: diag and "refute_params" :: thy_decl -uses "Tools/refute.ML" begin +ML_file "Tools/refute.ML" setup Refute.setup refute_params diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/SAT.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,10 +9,10 @@ theory SAT imports Refute -uses - "Tools/sat_funcs.ML" begin +ML_file "Tools/sat_funcs.ML" + ML {* structure sat = SATFunc(cnf) *} method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/SPARK/SPARK_Setup.thy --- a/src/HOL/SPARK/SPARK_Setup.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/SPARK/SPARK_Setup.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,13 +10,11 @@ keywords "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and "spark_vc" :: thy_goal and "spark_status" :: diag -uses - "Tools/fdl_lexer.ML" - "Tools/fdl_parser.ML" - ("Tools/spark_vcs.ML") - ("Tools/spark_commands.ML") begin +ML_file "Tools/fdl_lexer.ML" +ML_file "Tools/fdl_parser.ML" + text {* SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual *} @@ -180,8 +178,8 @@ text {* Load the package *} -use "Tools/spark_vcs.ML" -use "Tools/spark_commands.ML" +ML_file "Tools/spark_vcs.ML" +ML_file "Tools/spark_commands.ML" setup SPARK_Commands.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Semiring_Normalization.thy --- a/src/HOL/Semiring_Normalization.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Semiring_Normalization.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,10 +6,10 @@ theory Semiring_Normalization imports Numeral_Simprocs Nat_Transfer -uses - "Tools/semiring_normalizer.ML" begin +ML_file "Tools/semiring_normalizer.ML" + text {* Prelude *} class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,17 +9,18 @@ theory Sledgehammer imports ATP SMT keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl -uses "Tools/Sledgehammer/async_manager.ML" - "Tools/Sledgehammer/sledgehammer_util.ML" - "Tools/Sledgehammer/sledgehammer_fact.ML" - "Tools/Sledgehammer/sledgehammer_provers.ML" - "Tools/Sledgehammer/sledgehammer_minimize.ML" - "Tools/Sledgehammer/sledgehammer_mepo.ML" - "Tools/Sledgehammer/sledgehammer_mash.ML" - "Tools/Sledgehammer/sledgehammer_run.ML" - "Tools/Sledgehammer/sledgehammer_isar.ML" begin +ML_file "Tools/Sledgehammer/async_manager.ML" +ML_file "Tools/Sledgehammer/sledgehammer_util.ML" +ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" +ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" +ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" +ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" +ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" +ML_file "Tools/Sledgehammer/sledgehammer_run.ML" +ML_file "Tools/Sledgehammer/sledgehammer_isar.ML" + setup {* Sledgehammer_Isar.setup *} end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory DistinctTreeProver imports Main -uses ("distinct_tree_prover.ML") begin text {* A state space manages a set of (abstract) names and assumes @@ -631,7 +630,7 @@ text {* Now we have all the theorems in place that are needed for the certificate generating ML functions. *} -use "distinct_tree_prover.ML" +ML_file "distinct_tree_prover.ML" (* Uncomment for profiling or debugging *) (* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Statespace/StateSpaceLocale.thy --- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory StateSpaceLocale imports StateFun keywords "statespace" :: thy_decl -uses "state_space.ML" "state_fun.ML" begin +ML_file "state_space.ML" +ML_file "state_fun.ML" setup StateFun.setup text {* For every type that is to be stored in a state space, an diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/String.thy --- a/src/HOL/String.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/String.thy Wed Aug 22 22:55:41 2012 +0200 @@ -4,9 +4,6 @@ theory String imports List -uses - ("Tools/string_syntax.ML") - ("Tools/string_code.ML") begin subsection {* Characters *} @@ -79,7 +76,7 @@ syntax "_String" :: "str_position => string" ("_") -use "Tools/string_syntax.ML" +ML_file "Tools/string_syntax.ML" setup String_Syntax.setup definition chars :: string where @@ -188,7 +185,7 @@ subsection {* Code generator *} -use "Tools/string_code.ML" +ML_file "Tools/string_code.ML" code_reserved SML string code_reserved OCaml string diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/ATP_Problem_Import.thy --- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,10 +6,10 @@ theory ATP_Problem_Import imports Complex_Main TPTP_Interpret -uses "sledgehammer_tactics.ML" - ("atp_problem_import.ML") begin +ML_file "sledgehammer_tactics.ML" + ML {* Proofterm.proofs := 0 *} declare [[show_consts]] (* for Refute *) @@ -18,7 +18,7 @@ declare [[unify_search_bound = 60]] declare [[unify_trace_bound = 60]] -use "atp_problem_import.ML" +ML_file "atp_problem_import.ML" (* ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50 diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory ATP_Theory_Export imports Complex_Main -uses "atp_theory_export.ML" begin +ML_file "atp_theory_export.ML" + ML {* open ATP_Problem open ATP_Theory_Export diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory MaSh_Eval imports Complex_Main -uses "mash_eval.ML" begin +ML_file "mash_eval.ML" + sledgehammer_params [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory MaSh_Export imports Complex_Main -uses "mash_export.ML" begin +ML_file "mash_export.ML" + sledgehammer_params [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/TPTP_Interpret.thy --- a/src/HOL/TPTP/TPTP_Interpret.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Interpret.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,9 +8,10 @@ theory TPTP_Interpret imports Main TPTP_Parser keywords "import_tptp" :: thy_decl -uses ("TPTP_Parser/tptp_interpret.ML") +begin + +typedecl "ind" -begin -typedecl "ind" -use "TPTP_Parser/tptp_interpret.ML" +ML_file "TPTP_Parser/tptp_interpret.ML" + end \ No newline at end of file diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/TPTP_Parser.thy --- a/src/HOL/TPTP/TPTP_Parser.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,16 +6,15 @@ theory TPTP_Parser imports Pure -uses - "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*) +begin + +ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*) - "TPTP_Parser/tptp_syntax.ML" - "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) - "TPTP_Parser/tptp_parser.ML" - "TPTP_Parser/tptp_problem_name.ML" - "TPTP_Parser/tptp_proof.ML" - -begin +ML_file "TPTP_Parser/tptp_syntax.ML" +ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*) +ML_file "TPTP_Parser/tptp_parser.ML" +ML_file "TPTP_Parser/tptp_problem_name.ML" +ML_file "TPTP_Parser/tptp_proof.ML" text {*The TPTP parser was generated using ML-Yacc, and needs the ML-Yacc library to operate. This library is included with the parser, diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/TPTP_Parser_Example.thy --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ theory TPTP_Parser_Example imports TPTP_Parser TPTP_Interpret -uses "sledgehammer_tactics.ML" begin +ML_file "sledgehammer_tactics.ML" + import_tptp "$TPTP/Problems/CSR/CSR077+1.p" ML {* diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Transfer.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,6 @@ theory Transfer imports Plain Hilbert_Choice -uses ("Tools/transfer.ML") begin subsection {* Relator for function space *} @@ -96,8 +95,7 @@ shows "Rel (A ===> B) (\x. f x) (\y. g y)" using assms unfolding Rel_def fun_rel_def by fast -use "Tools/transfer.ML" - +ML_file "Tools/transfer.ML" setup Transfer.setup declare fun_rel_eq [relator_eq] diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Transitive_Closure.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,10 @@ theory Transitive_Closure imports Relation -uses "~~/src/Provers/trancl.ML" begin +ML_file "~~/src/Provers/trancl.ML" + text {* @{text rtrancl} is reflexive/transitive closure, @{text trancl} is transitive closure, diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Typedef.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Typedef imports Set keywords "typedef" :: thy_goal and "morphisms" -uses ("Tools/typedef.ML") begin locale type_definition = @@ -109,6 +108,6 @@ end -use "Tools/typedef.ML" setup Typedef.setup +ML_file "Tools/typedef.ML" setup Typedef.setup end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,9 +7,10 @@ theory UNITY_Main imports Detects PPROD Follows ProgressSets -uses "UNITY_tactics.ML" begin +ML_file "UNITY_tactics.ML" + method_setup safety = {* Scan.succeed (SIMPLE_METHOD' o constrains_tac) *} "for proving safety properties" diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Wellfounded.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,7 +9,6 @@ theory Wellfounded imports Transitive_Closure -uses ("Tools/Function/size.ML") begin subsection {* Basic Definitions *} @@ -845,8 +844,7 @@ subsection {* size of a datatype value *} -use "Tools/Function/size.ML" - +ML_file "Tools/Function/size.ML" setup Size.setup lemma size_bool [code]: diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Word/Word.thy Wed Aug 22 22:55:41 2012 +0200 @@ -10,9 +10,6 @@ Misc_Typedef "~~/src/HOL/Library/Boolean_Algebra" Bool_List_Representation -uses - ("~~/src/HOL/Word/Tools/smt_word.ML") - ("~~/src/HOL/Word/Tools/word_lib.ML") begin text {* see @{text "Examples/WordExamples.thy"} for examples *} @@ -4647,8 +4644,8 @@ declare bin_to_bl_def [simp] -use "~~/src/HOL/Word/Tools/word_lib.ML" -use "~~/src/HOL/Word/Tools/smt_word.ML" +ML_file "~~/src/HOL/Word/Tools/word_lib.ML" +ML_file "~~/src/HOL/Word/Tools/smt_word.ML" setup {* SMT_Word.setup *} hide_const (open) Word diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/ex/Interpretation_with_Defs.thy --- a/src/HOL/ex/Interpretation_with_Defs.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/ex/Interpretation_with_Defs.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,7 +6,8 @@ theory Interpretation_with_Defs imports Pure -uses "~~/src/Tools/interpretation_with_defs.ML" begin +ML_file "~~/src/Tools/interpretation_with_defs.ML" + end diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Wed Aug 22 22:55:41 2012 +0200 @@ -9,9 +9,10 @@ theory SVC_Oracle imports Main -uses "svc_funcs.ML" begin +ML_file "svc_funcs.ML" + consts iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool" diff -r d72ca5742f80 -r c0eafbd55de3 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Pure/Pure.thy Wed Aug 22 22:55:41 2012 +0200 @@ -85,12 +85,13 @@ and "end" :: thy_end % "theory" and "realizers" "realizability" "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag - uses - "Isar/isar_syn.ML" - "Tools/find_theorems.ML" - "Tools/find_consts.ML" begin +ML_file "Isar/isar_syn.ML" +ML_file "Tools/find_theorems.ML" +ML_file "Tools/find_consts.ML" + + section {* Further content for the Pure theory *} subsection {* Meta-level connectives in assumptions *} diff -r d72ca5742f80 -r c0eafbd55de3 src/Sequents/LK.thy --- a/src/Sequents/LK.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Sequents/LK.thy Wed Aug 22 22:55:41 2012 +0200 @@ -14,7 +14,6 @@ theory LK imports LK0 -uses ("simpdata.ML") begin axiomatization where @@ -215,7 +214,7 @@ apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *}) done -use "simpdata.ML" +ML_file "simpdata.ML" setup {* Simplifier.map_simpset_global (K LK_ss) *} diff -r d72ca5742f80 -r c0eafbd55de3 src/Sequents/Modal0.thy --- a/src/Sequents/Modal0.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Sequents/Modal0.thy Wed Aug 22 22:55:41 2012 +0200 @@ -5,9 +5,10 @@ theory Modal0 imports LK0 -uses "modal.ML" begin +ML_file "modal.ML" + consts box :: "o=>o" ("[]_" [50] 50) dia :: "o=>o" ("<>_" [50] 50) diff -r d72ca5742f80 -r c0eafbd55de3 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Sequents/Sequents.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,7 +7,6 @@ theory Sequents imports Pure -uses ("prover.ML") begin setup Pure_Thy.old_appl_syntax_setup @@ -142,7 +141,7 @@ parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *} -use "prover.ML" +ML_file "prover.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Tools/Code_Generator.thy Wed Aug 22 22:55:41 2012 +0200 @@ -12,22 +12,20 @@ "code_const" "code_reserved" "code_include" "code_modulename" "code_abort" "code_monad" "code_reflect" :: thy_decl and "datatypes" "functions" "module_name" "file" "checking" -uses - "~~/src/Tools/value.ML" - "~~/src/Tools/cache_io.ML" - "~~/src/Tools/Code/code_preproc.ML" - "~~/src/Tools/Code/code_thingol.ML" - "~~/src/Tools/Code/code_simp.ML" - "~~/src/Tools/Code/code_printer.ML" - "~~/src/Tools/Code/code_target.ML" - "~~/src/Tools/Code/code_namespace.ML" - "~~/src/Tools/Code/code_ml.ML" - "~~/src/Tools/Code/code_haskell.ML" - "~~/src/Tools/Code/code_scala.ML" - ("~~/src/Tools/Code/code_runtime.ML") - ("~~/src/Tools/nbe.ML") begin +ML_file "~~/src/Tools/value.ML" +ML_file "~~/src/Tools/cache_io.ML" +ML_file "~~/src/Tools/Code/code_preproc.ML" +ML_file "~~/src/Tools/Code/code_thingol.ML" +ML_file "~~/src/Tools/Code/code_simp.ML" +ML_file "~~/src/Tools/Code/code_printer.ML" +ML_file "~~/src/Tools/Code/code_target.ML" +ML_file "~~/src/Tools/Code/code_namespace.ML" +ML_file "~~/src/Tools/Code/code_ml.ML" +ML_file "~~/src/Tools/Code/code_haskell.ML" +ML_file "~~/src/Tools/Code/code_scala.ML" + setup {* Value.setup #> Code_Preproc.setup @@ -65,9 +63,8 @@ by rule (rule holds)+ qed -use "~~/src/Tools/Code/code_runtime.ML" -use "~~/src/Tools/nbe.ML" - +ML_file "~~/src/Tools/Code/code_runtime.ML" +ML_file "~~/src/Tools/nbe.ML" setup Nbe.setup hide_const (open) holds diff -r d72ca5742f80 -r c0eafbd55de3 src/Tools/WWW_Find/WWW_Find.thy --- a/src/Tools/WWW_Find/WWW_Find.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/Tools/WWW_Find/WWW_Find.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,20 +1,20 @@ theory WWW_Find imports Pure -uses - "unicode_symbols.ML" - "html_unicode.ML" - "mime.ML" - "http_status.ML" - "http_util.ML" - "xhtml.ML" - "socket_util.ML" - "scgi_req.ML" - "scgi_server.ML" - "echo.ML" - "html_templates.ML" - "find_theorems.ML" - "yxml_find_theorems.ML" begin +ML_file "unicode_symbols.ML" +ML_file "html_unicode.ML" +ML_file "mime.ML" +ML_file "http_status.ML" +ML_file "http_util.ML" +ML_file "xhtml.ML" +ML_file "socket_util.ML" +ML_file "scgi_req.ML" +ML_file "scgi_server.ML" +ML_file "echo.ML" +ML_file "html_templates.ML" +ML_file "find_theorems.ML" +ML_file "yxml_find_theorems.ML" + end diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/ArithSimp.thy --- a/src/ZF/ArithSimp.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/ArithSimp.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,11 +7,13 @@ theory ArithSimp imports Arith -uses "~~/src/Provers/Arith/cancel_numerals.ML" - "~~/src/Provers/Arith/combine_numerals.ML" - "arith_data.ML" begin +ML_file "~~/src/Provers/Arith/cancel_numerals.ML" +ML_file "~~/src/Provers/Arith/combine_numerals.ML" +ML_file "arith_data.ML" + + subsection{*Difference*} lemma diff_self_eq_0 [simp]: "m #- m = 0" diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/Bin.thy Wed Aug 22 22:55:41 2012 +0200 @@ -17,7 +17,6 @@ theory Bin imports Int_ZF Datatype_ZF -uses ("Tools/numeral_syntax.ML") begin consts bin :: i @@ -104,7 +103,7 @@ syntax "_Int" :: "xnum_token => i" ("_") -use "Tools/numeral_syntax.ML" +ML_file "Tools/numeral_syntax.ML" setup Numeral_Syntax.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/Datatype_ZF.thy --- a/src/ZF/Datatype_ZF.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/Datatype_ZF.thy Wed Aug 22 22:55:41 2012 +0200 @@ -8,9 +8,10 @@ theory Datatype_ZF imports Inductive_ZF Univ QUniv keywords "datatype" "codatatype" :: thy_decl -uses "Tools/datatype_package.ML" begin +ML_file "Tools/datatype_package.ML" + ML {* (*Typechecking rules for most datatypes involving univ*) structure Data_Arg = diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/Inductive_ZF.thy --- a/src/ZF/Inductive_ZF.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/Inductive_ZF.thy Wed Aug 22 22:55:41 2012 +0200 @@ -18,13 +18,6 @@ "inductive_cases" :: thy_script and "domains" "intros" "monos" "con_defs" "type_intros" "type_elims" "elimination" "induction" "case_eqns" "recursor_eqns" -uses - ("ind_syntax.ML") - ("Tools/cartprod.ML") - ("Tools/ind_cases.ML") - ("Tools/inductive_package.ML") - ("Tools/induct_tacs.ML") - ("Tools/primrec_package.ML") begin lemma def_swap_iff: "a == b ==> a = c \ c = b" @@ -35,12 +28,12 @@ lemma refl_thin: "!!P. a = a ==> P ==> P" . -use "ind_syntax.ML" -use "Tools/ind_cases.ML" -use "Tools/cartprod.ML" -use "Tools/inductive_package.ML" -use "Tools/induct_tacs.ML" -use "Tools/primrec_package.ML" +ML_file "ind_syntax.ML" +ML_file "Tools/ind_cases.ML" +ML_file "Tools/cartprod.ML" +ML_file "Tools/inductive_package.ML" +ML_file "Tools/induct_tacs.ML" +ML_file "Tools/primrec_package.ML" setup IndCases.setup setup DatatypeTactics.setup diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/IntArith.thy --- a/src/ZF/IntArith.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/IntArith.thy Wed Aug 22 22:55:41 2012 +0200 @@ -1,6 +1,5 @@ theory IntArith imports Bin -uses ("int_arith.ML") begin @@ -90,6 +89,6 @@ apply (simp add: zadd_ac) done -use "int_arith.ML" +ML_file "int_arith.ML" end diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/pair.thy --- a/src/ZF/pair.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/pair.thy Wed Aug 22 22:55:41 2012 +0200 @@ -6,9 +6,10 @@ header{*Ordered Pairs*} theory pair imports upair -uses "simpdata.ML" begin +ML_file "simpdata.ML" + setup {* Simplifier.map_simpset_global (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) diff -r d72ca5742f80 -r c0eafbd55de3 src/ZF/upair.thy --- a/src/ZF/upair.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/ZF/upair.thy Wed Aug 22 22:55:41 2012 +0200 @@ -14,9 +14,9 @@ theory upair imports ZF keywords "print_tcset" :: diag -uses "Tools/typechk.ML" begin +ML_file "Tools/typechk.ML" setup TypeCheck.setup lemma atomize_ball [symmetric, rulify]: