prefer ML_file over old uses;
authorwenzelm
Wed Aug 22 22:55:41 2012 +0200 (2012-08-22)
changeset 48891c0eafbd55de3
parent 48890 d72ca5742f80
child 48892 0b2407f406e8
prefer ML_file over old uses;
doc-src/Classes/Thy/Setup.thy
doc-src/Codegen/Thy/Setup.thy
doc-src/IsarImplementation/Thy/Base.thy
doc-src/IsarRef/Thy/Base.thy
doc-src/System/Thy/Base.thy
doc-src/TutorialI/Types/Setup.thy
src/CTT/CTT.thy
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/HOL/ATP.thy
src/HOL/Algebra/Ring.thy
src/HOL/Boogie/Boogie.thy
src/HOL/Code_Evaluation.thy
src/HOL/Datatype.thy
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Divides.thy
src/HOL/Extraction.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/FunDef.thy
src/HOL/Groebner_Basis.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/IOA/ABP/Correctness.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Import/Import_Setup.thy
src/HOL/Inductive.thy
src/HOL/Int.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Library/Code_Prolog.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Sum_of_Squares.thy
src/HOL/Lifting.thy
src/HOL/List.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy
src/HOL/Matrix_LP/Cplex.thy
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/Mirabelle_Test.thy
src/HOL/Multivariate_Analysis/Norm_Arith.thy
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/MutabelleExtra.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Nat_Transfer.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Num.thy
src/HOL/Numeral_Simprocs.thy
src/HOL/Orderings.thy
src/HOL/Partial_Function.thy
src/HOL/Predicate_Compile.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Prolog/HOHH.thy
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quotient.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Record.thy
src/HOL/Refute.thy
src/HOL/SAT.thy
src/HOL/SPARK/SPARK_Setup.thy
src/HOL/Semiring_Normalization.thy
src/HOL/Sledgehammer.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/String.thy
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/ATP_Theory_Export.thy
src/HOL/TPTP/MaSh_Eval.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/TPTP_Interpret.thy
src/HOL/TPTP/TPTP_Parser.thy
src/HOL/TPTP/TPTP_Parser_Example.thy
src/HOL/Transfer.thy
src/HOL/Transitive_Closure.thy
src/HOL/Typedef.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/Wellfounded.thy
src/HOL/Word/Word.thy
src/HOL/ex/Interpretation_with_Defs.thy
src/HOL/ex/SVC_Oracle.thy
src/Pure/Pure.thy
src/Sequents/LK.thy
src/Sequents/Modal0.thy
src/Sequents/Sequents.thy
src/Tools/Code_Generator.thy
src/Tools/WWW_Find/WWW_Find.thy
src/ZF/ArithSimp.thy
src/ZF/Bin.thy
src/ZF/Datatype_ZF.thy
src/ZF/Inductive_ZF.thy
src/ZF/IntArith.thy
src/ZF/pair.thy
src/ZF/upair.thy
     1.1 --- a/doc-src/Classes/Thy/Setup.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/doc-src/Classes/Thy/Setup.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -1,10 +1,10 @@
     1.4  theory Setup
     1.5  imports Main "~~/src/HOL/Library/Code_Integer"
     1.6 -uses
     1.7 -  "../../antiquote_setup.ML"
     1.8 -  "../../more_antiquote.ML"
     1.9  begin
    1.10  
    1.11 +ML_file "../../antiquote_setup.ML"
    1.12 +ML_file "../../more_antiquote.ML"
    1.13 +
    1.14  setup {*
    1.15    Antiquote_Setup.setup #>
    1.16    More_Antiquote.setup #>
     2.1 --- a/doc-src/Codegen/Thy/Setup.thy	Wed Aug 22 22:47:16 2012 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Wed Aug 22 22:55:41 2012 +0200
     2.3 @@ -4,11 +4,11 @@
     2.4    "~~/src/HOL/Library/Dlist"
     2.5    "~~/src/HOL/Library/RBT"
     2.6    "~~/src/HOL/Library/Mapping"
     2.7 -uses
     2.8 -  "../../antiquote_setup.ML"
     2.9 -  "../../more_antiquote.ML"
    2.10  begin
    2.11  
    2.12 +ML_file "../../antiquote_setup.ML"
    2.13 +ML_file "../../more_antiquote.ML"
    2.14 +
    2.15  setup {*
    2.16    Antiquote_Setup.setup #>
    2.17    More_Antiquote.setup #>
     3.1 --- a/doc-src/IsarImplementation/Thy/Base.thy	Wed Aug 22 22:47:16 2012 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/Base.thy	Wed Aug 22 22:55:41 2012 +0200
     3.3 @@ -1,8 +1,8 @@
     3.4  theory Base
     3.5  imports Main
     3.6 -uses "../../antiquote_setup.ML"
     3.7  begin
     3.8  
     3.9 +ML_file "../../antiquote_setup.ML"
    3.10  setup {* Antiquote_Setup.setup *}
    3.11  
    3.12  end
     4.1 --- a/doc-src/IsarRef/Thy/Base.thy	Wed Aug 22 22:47:16 2012 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Base.thy	Wed Aug 22 22:55:41 2012 +0200
     4.3 @@ -1,8 +1,9 @@
     4.4  theory Base
     4.5  imports Pure
     4.6 -uses "../../antiquote_setup.ML"
     4.7  begin
     4.8  
     4.9 +ML_file "../../antiquote_setup.ML"
    4.10 +
    4.11  setup {*
    4.12    Antiquote_Setup.setup #>
    4.13    member (op =) (Session.id ()) "ZF" ? Pure_Thy.old_appl_syntax_setup
     5.1 --- a/doc-src/System/Thy/Base.thy	Wed Aug 22 22:47:16 2012 +0200
     5.2 +++ b/doc-src/System/Thy/Base.thy	Wed Aug 22 22:55:41 2012 +0200
     5.3 @@ -1,9 +1,9 @@
     5.4  theory Base
     5.5  imports Pure
     5.6 -uses "../../antiquote_setup.ML"
     5.7  begin
     5.8  
     5.9 -setup {* Antiquote_Setup.setup *}
    5.10 +ML_file "../../antiquote_setup.ML"
    5.11 +setup Antiquote_Setup.setup
    5.12  
    5.13  declare [[thy_output_source]]
    5.14  
     6.1 --- a/doc-src/TutorialI/Types/Setup.thy	Wed Aug 22 22:47:16 2012 +0200
     6.2 +++ b/doc-src/TutorialI/Types/Setup.thy	Wed Aug 22 22:55:41 2012 +0200
     6.3 @@ -1,11 +1,10 @@
     6.4  theory Setup
     6.5  imports Main
     6.6 -uses
     6.7 -  "../../antiquote_setup.ML"
     6.8 -  "../../more_antiquote.ML"
     6.9  begin
    6.10  
    6.11 +ML_file "../../antiquote_setup.ML"
    6.12 +ML_file "../../more_antiquote.ML"
    6.13 +
    6.14  setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
    6.15  
    6.16 -
    6.17  end
    6.18 \ No newline at end of file
     7.1 --- a/src/CTT/CTT.thy	Wed Aug 22 22:47:16 2012 +0200
     7.2 +++ b/src/CTT/CTT.thy	Wed Aug 22 22:55:41 2012 +0200
     7.3 @@ -7,9 +7,9 @@
     7.4  
     7.5  theory CTT
     7.6  imports Pure
     7.7 -uses "~~/src/Provers/typedsimp.ML" ("rew.ML")
     7.8  begin
     7.9  
    7.10 +ML_file "~~/src/Provers/typedsimp.ML"
    7.11  setup Pure_Thy.old_appl_syntax_setup
    7.12  
    7.13  typedecl i
    7.14 @@ -460,7 +460,7 @@
    7.15  fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
    7.16  *}
    7.17  
    7.18 -use "rew.ML"
    7.19 +ML_file "rew.ML"
    7.20  
    7.21  
    7.22  subsection {* The elimination rules for fst/snd *}
     8.1 --- a/src/FOL/FOL.thy	Wed Aug 22 22:47:16 2012 +0200
     8.2 +++ b/src/FOL/FOL.thy	Wed Aug 22 22:55:41 2012 +0200
     8.3 @@ -7,15 +7,14 @@
     8.4  theory FOL
     8.5  imports IFOL
     8.6  keywords "print_claset" "print_induct_rules" :: diag
     8.7 -uses
     8.8 -  "~~/src/Provers/classical.ML"
     8.9 -  "~~/src/Provers/blast.ML"
    8.10 -  "~~/src/Provers/clasimp.ML"
    8.11 -  "~~/src/Tools/induct.ML"
    8.12 -  "~~/src/Tools/case_product.ML"
    8.13 -  ("simpdata.ML")
    8.14  begin
    8.15  
    8.16 +ML_file "~~/src/Provers/classical.ML"
    8.17 +ML_file "~~/src/Provers/blast.ML"
    8.18 +ML_file "~~/src/Provers/clasimp.ML"
    8.19 +ML_file "~~/src/Tools/induct.ML"
    8.20 +ML_file "~~/src/Tools/case_product.ML"
    8.21 +
    8.22  
    8.23  subsection {* The classical axiom *}
    8.24  
    8.25 @@ -329,7 +328,7 @@
    8.26    not_imp not_all not_ex cases_simp cla_simps_misc
    8.27  
    8.28  
    8.29 -use "simpdata.ML"
    8.30 +ML_file "simpdata.ML"
    8.31  
    8.32  simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
    8.33  simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
     9.1 --- a/src/FOL/IFOL.thy	Wed Aug 22 22:47:16 2012 +0200
     9.2 +++ b/src/FOL/IFOL.thy	Wed Aug 22 22:55:41 2012 +0200
     9.3 @@ -6,23 +6,21 @@
     9.4  
     9.5  theory IFOL
     9.6  imports Pure
     9.7 -uses
     9.8 -  "~~/src/Tools/misc_legacy.ML"
     9.9 -  "~~/src/Provers/splitter.ML"
    9.10 -  "~~/src/Provers/hypsubst.ML"
    9.11 -  "~~/src/Tools/IsaPlanner/zipper.ML"
    9.12 -  "~~/src/Tools/IsaPlanner/isand.ML"
    9.13 -  "~~/src/Tools/IsaPlanner/rw_tools.ML"
    9.14 -  "~~/src/Tools/IsaPlanner/rw_inst.ML"
    9.15 -  "~~/src/Tools/eqsubst.ML"
    9.16 -  "~~/src/Provers/quantifier1.ML"
    9.17 -  "~~/src/Tools/intuitionistic.ML"
    9.18 -  "~~/src/Tools/project_rule.ML"
    9.19 -  "~~/src/Tools/atomize_elim.ML"
    9.20 -  ("fologic.ML")
    9.21 -  ("intprover.ML")
    9.22  begin
    9.23  
    9.24 +ML_file "~~/src/Tools/misc_legacy.ML"
    9.25 +ML_file "~~/src/Provers/splitter.ML"
    9.26 +ML_file "~~/src/Provers/hypsubst.ML"
    9.27 +ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
    9.28 +ML_file "~~/src/Tools/IsaPlanner/isand.ML"
    9.29 +ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
    9.30 +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
    9.31 +ML_file "~~/src/Tools/eqsubst.ML"
    9.32 +ML_file "~~/src/Provers/quantifier1.ML"
    9.33 +ML_file "~~/src/Tools/intuitionistic.ML"
    9.34 +ML_file "~~/src/Tools/project_rule.ML"
    9.35 +ML_file "~~/src/Tools/atomize_elim.ML"
    9.36 +
    9.37  
    9.38  subsection {* Syntax and axiomatic basis *}
    9.39  
    9.40 @@ -575,7 +573,7 @@
    9.41  )
    9.42  *}
    9.43  
    9.44 -use "fologic.ML"
    9.45 +ML_file "fologic.ML"
    9.46  
    9.47  lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
    9.48  
    9.49 @@ -597,7 +595,7 @@
    9.50  *}
    9.51  
    9.52  setup hypsubst_setup
    9.53 -use "intprover.ML"
    9.54 +ML_file "intprover.ML"
    9.55  
    9.56  
    9.57  subsection {* Intuitionistic Reasoning *}
    10.1 --- a/src/FOLP/FOLP.thy	Wed Aug 22 22:47:16 2012 +0200
    10.2 +++ b/src/FOLP/FOLP.thy	Wed Aug 22 22:55:41 2012 +0200
    10.3 @@ -7,8 +7,6 @@
    10.4  
    10.5  theory FOLP
    10.6  imports IFOLP
    10.7 -uses
    10.8 -  ("classical.ML") ("simp.ML") ("simpdata.ML")
    10.9  begin
   10.10  
   10.11  axiomatization cla :: "[p=>p]=>p"
   10.12 @@ -99,8 +97,8 @@
   10.13    apply assumption
   10.14    done
   10.15  
   10.16 -use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
   10.17 -use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
   10.18 +ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)
   10.19 +ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)
   10.20  
   10.21  ML {*
   10.22  structure Cla = Classical
   10.23 @@ -139,6 +137,6 @@
   10.24    apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
   10.25    done
   10.26  
   10.27 -use "simpdata.ML"
   10.28 +ML_file "simpdata.ML"
   10.29  
   10.30  end
    11.1 --- a/src/FOLP/IFOLP.thy	Wed Aug 22 22:47:16 2012 +0200
    11.2 +++ b/src/FOLP/IFOLP.thy	Wed Aug 22 22:55:41 2012 +0200
    11.3 @@ -7,9 +7,10 @@
    11.4  
    11.5  theory IFOLP
    11.6  imports Pure
    11.7 -uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML")
    11.8  begin
    11.9  
   11.10 +ML_file "~~/src/Tools/misc_legacy.ML"
   11.11 +
   11.12  setup Pure_Thy.old_appl_syntax_setup
   11.13  
   11.14  classes "term"
   11.15 @@ -587,7 +588,7 @@
   11.16  
   11.17  lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
   11.18  
   11.19 -use "hypsubst.ML"
   11.20 +ML_file "hypsubst.ML"
   11.21  
   11.22  ML {*
   11.23  structure Hypsubst = Hypsubst
   11.24 @@ -609,7 +610,7 @@
   11.25  open Hypsubst;
   11.26  *}
   11.27  
   11.28 -use "intprover.ML"
   11.29 +ML_file "intprover.ML"
   11.30  
   11.31  
   11.32  (*** Rewrite rules ***)
    12.1 --- a/src/HOL/ATP.thy	Wed Aug 22 22:47:16 2012 +0200
    12.2 +++ b/src/HOL/ATP.thy	Wed Aug 22 22:55:41 2012 +0200
    12.3 @@ -7,17 +7,15 @@
    12.4  
    12.5  theory ATP
    12.6  imports Meson
    12.7 -uses "Tools/lambda_lifting.ML"
    12.8 -     "Tools/monomorph.ML"
    12.9 -     "Tools/ATP/atp_util.ML"
   12.10 -     "Tools/ATP/atp_problem.ML"
   12.11 -     "Tools/ATP/atp_proof.ML"
   12.12 -     "Tools/ATP/atp_proof_redirect.ML"
   12.13 -     ("Tools/ATP/atp_problem_generate.ML")
   12.14 -     ("Tools/ATP/atp_proof_reconstruct.ML")
   12.15 -     ("Tools/ATP/atp_systems.ML")
   12.16  begin
   12.17  
   12.18 +ML_file "Tools/lambda_lifting.ML"
   12.19 +ML_file "Tools/monomorph.ML"
   12.20 +ML_file "Tools/ATP/atp_util.ML"
   12.21 +ML_file "Tools/ATP/atp_problem.ML"
   12.22 +ML_file "Tools/ATP/atp_proof.ML"
   12.23 +ML_file "Tools/ATP/atp_proof_redirect.ML"
   12.24 +
   12.25  subsection {* Higher-order reasoning helpers *}
   12.26  
   12.27  definition fFalse :: bool where [no_atp]:
   12.28 @@ -132,9 +130,9 @@
   12.29  
   12.30  subsection {* Setup *}
   12.31  
   12.32 -use "Tools/ATP/atp_problem_generate.ML"
   12.33 -use "Tools/ATP/atp_proof_reconstruct.ML"
   12.34 -use "Tools/ATP/atp_systems.ML"
   12.35 +ML_file "Tools/ATP/atp_problem_generate.ML"
   12.36 +ML_file "Tools/ATP/atp_proof_reconstruct.ML"
   12.37 +ML_file "Tools/ATP/atp_systems.ML"
   12.38  
   12.39  setup ATP_Systems.setup
   12.40  
    13.1 --- a/src/HOL/Algebra/Ring.thy	Wed Aug 22 22:47:16 2012 +0200
    13.2 +++ b/src/HOL/Algebra/Ring.thy	Wed Aug 22 22:55:41 2012 +0200
    13.3 @@ -5,7 +5,6 @@
    13.4  
    13.5  theory Ring
    13.6  imports FiniteProduct
    13.7 -uses ("ringsimp.ML")
    13.8  begin
    13.9  
   13.10  section {* The Algebraic Hierarchy of Rings *}
   13.11 @@ -389,7 +388,7 @@
   13.12  text {* Setup algebra method:
   13.13    compute distributive normal form in locale contexts *}
   13.14  
   13.15 -use "ringsimp.ML"
   13.16 +ML_file "ringsimp.ML"
   13.17  
   13.18  setup Algebra.attrib_setup
   13.19  
    14.1 --- a/src/HOL/Boogie/Boogie.thy	Wed Aug 22 22:47:16 2012 +0200
    14.2 +++ b/src/HOL/Boogie/Boogie.thy	Wed Aug 22 22:55:41 2012 +0200
    14.3 @@ -8,11 +8,6 @@
    14.4  imports Word
    14.5  keywords
    14.6    "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag
    14.7 -uses
    14.8 -  ("Tools/boogie_vcs.ML")
    14.9 -  ("Tools/boogie_loader.ML")
   14.10 -  ("Tools/boogie_tactics.ML")
   14.11 -  ("Tools/boogie_commands.ML")
   14.12  begin
   14.13  
   14.14  text {*
   14.15 @@ -95,12 +90,12 @@
   14.16  *}
   14.17  setup Boogie_Axioms.setup
   14.18  
   14.19 -use "Tools/boogie_vcs.ML"
   14.20 -use "Tools/boogie_loader.ML"
   14.21 -use "Tools/boogie_tactics.ML"
   14.22 +ML_file "Tools/boogie_vcs.ML"
   14.23 +ML_file "Tools/boogie_loader.ML"
   14.24 +ML_file "Tools/boogie_tactics.ML"
   14.25  setup Boogie_Tactics.setup
   14.26  
   14.27 -use "Tools/boogie_commands.ML"
   14.28 +ML_file "Tools/boogie_commands.ML"
   14.29  setup Boogie_Commands.setup
   14.30  
   14.31  end
    15.1 --- a/src/HOL/Code_Evaluation.thy	Wed Aug 22 22:47:16 2012 +0200
    15.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Aug 22 22:55:41 2012 +0200
    15.3 @@ -6,7 +6,6 @@
    15.4  
    15.5  theory Code_Evaluation
    15.6  imports Plain Typerep Code_Numeral Predicate
    15.7 -uses ("Tools/code_evaluation.ML")
    15.8  begin
    15.9  
   15.10  subsection {* Term representation *}
   15.11 @@ -73,7 +72,7 @@
   15.12    shows "x \<equiv> y"
   15.13    using assms by simp
   15.14  
   15.15 -use "Tools/code_evaluation.ML"
   15.16 +ML_file "Tools/code_evaluation.ML"
   15.17  
   15.18  code_reserved Eval Code_Evaluation
   15.19  
    16.1 --- a/src/HOL/Datatype.thy	Wed Aug 22 22:47:16 2012 +0200
    16.2 +++ b/src/HOL/Datatype.thy	Wed Aug 22 22:55:41 2012 +0200
    16.3 @@ -8,10 +8,6 @@
    16.4  theory Datatype
    16.5  imports Product_Type Sum_Type Nat
    16.6  keywords "datatype" :: thy_decl
    16.7 -uses
    16.8 -  ("Tools/Datatype/datatype.ML")
    16.9 -  ("Tools/inductive_realizer.ML")
   16.10 -  ("Tools/Datatype/datatype_realizer.ML")
   16.11  begin
   16.12  
   16.13  subsection {* The datatype universe *}
   16.14 @@ -517,12 +513,12 @@
   16.15  hide_type (open) node item
   16.16  hide_const (open) Push Node Atom Leaf Numb Lim Split Case
   16.17  
   16.18 -use "Tools/Datatype/datatype.ML"
   16.19 +ML_file "Tools/Datatype/datatype.ML"
   16.20  
   16.21 -use "Tools/inductive_realizer.ML"
   16.22 +ML_file "Tools/inductive_realizer.ML"
   16.23  setup InductiveRealizer.setup
   16.24  
   16.25 -use "Tools/Datatype/datatype_realizer.ML"
   16.26 +ML_file "Tools/Datatype/datatype_realizer.ML"
   16.27  setup Datatype_Realizer.setup
   16.28  
   16.29  end
    17.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Aug 22 22:47:16 2012 +0200
    17.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Aug 22 22:55:41 2012 +0200
    17.3 @@ -7,7 +7,6 @@
    17.4  
    17.5  theory Commutative_Ring
    17.6  imports Main Parity
    17.7 -uses ("commutative_ring_tac.ML")
    17.8  begin
    17.9  
   17.10  text {* Syntax of multivariate polynomials (pol) and polynomial expressions. *}
   17.11 @@ -313,7 +312,7 @@
   17.12  qed
   17.13  
   17.14  
   17.15 -use "commutative_ring_tac.ML"
   17.16 +ML_file "commutative_ring_tac.ML"
   17.17  
   17.18  method_setup comm_ring = {*
   17.19    Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
    18.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Aug 22 22:47:16 2012 +0200
    18.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Aug 22 22:55:41 2012 +0200
    18.3 @@ -4,7 +4,6 @@
    18.4  
    18.5  theory Cooper
    18.6  imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
    18.7 -uses ("cooper_tac.ML")
    18.8  begin
    18.9  
   18.10  (* Periodicity of dvd *)
   18.11 @@ -2004,7 +2003,7 @@
   18.12  end;
   18.13  *}
   18.14  
   18.15 -use "cooper_tac.ML"
   18.16 +ML_file "cooper_tac.ML"
   18.17  
   18.18  method_setup cooper = {*
   18.19    Args.mode "no_quantify" >>
    19.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Aug 22 22:47:16 2012 +0200
    19.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Aug 22 22:55:41 2012 +0200
    19.3 @@ -7,13 +7,11 @@
    19.4  
    19.5  theory Dense_Linear_Order
    19.6  imports Main
    19.7 -uses
    19.8 -  "langford_data.ML"
    19.9 -  "ferrante_rackoff_data.ML"
   19.10 -  ("langford.ML")
   19.11 -  ("ferrante_rackoff.ML")
   19.12  begin
   19.13  
   19.14 +ML_file "langford_data.ML"
   19.15 +ML_file "ferrante_rackoff_data.ML"
   19.16 +
   19.17  setup {* Langford_Data.setup #> Ferrante_Rackoff_Data.setup *}
   19.18  
   19.19  context linorder
   19.20 @@ -290,7 +288,7 @@
   19.21  
   19.22  lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
   19.23  
   19.24 -use "langford.ML"
   19.25 +ML_file "langford.ML"
   19.26  method_setup dlo = {*
   19.27    Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
   19.28  *} "Langford's algorithm for quantifier elimination in dense linear orders"
   19.29 @@ -540,7 +538,7 @@
   19.30  
   19.31  end
   19.32  
   19.33 -use "ferrante_rackoff.ML"
   19.34 +ML_file "ferrante_rackoff.ML"
   19.35  
   19.36  method_setup ferrack = {*
   19.37    Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
    20.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Aug 22 22:47:16 2012 +0200
    20.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Aug 22 22:55:41 2012 +0200
    20.3 @@ -5,7 +5,6 @@
    20.4  theory Ferrack
    20.5  imports Complex_Main Dense_Linear_Order DP_Library
    20.6    "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
    20.7 -uses ("ferrack_tac.ML")
    20.8  begin
    20.9  
   20.10  section {* Quantifier elimination for @{text "\<real> (0, 1, +, <)"} *}
   20.11 @@ -2003,7 +2002,7 @@
   20.12  end;
   20.13  *}
   20.14  
   20.15 -use "ferrack_tac.ML"
   20.16 +ML_file "ferrack_tac.ML"
   20.17  
   20.18  method_setup rferrack = {*
   20.19    Args.mode "no_quantify" >>
    21.1 --- a/src/HOL/Decision_Procs/MIR.thy	Wed Aug 22 22:47:16 2012 +0200
    21.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Aug 22 22:55:41 2012 +0200
    21.3 @@ -5,7 +5,6 @@
    21.4  theory MIR
    21.5  imports Complex_Main Dense_Linear_Order DP_Library
    21.6    "~~/src/HOL/Library/Efficient_Nat" "~~/src/HOL/Library/Old_Recdef"
    21.7 -uses ("mir_tac.ML")
    21.8  begin
    21.9  
   21.10  section {* Quantifier elimination for @{text "\<real> (0, 1, +, floor, <)"} *}
   21.11 @@ -5634,7 +5633,7 @@
   21.12  end;
   21.13  *}
   21.14  
   21.15 -use "mir_tac.ML"
   21.16 +ML_file "mir_tac.ML"
   21.17  
   21.18  method_setup mir = {*
   21.19    Args.mode "no_quantify" >>
    22.1 --- a/src/HOL/Divides.thy	Wed Aug 22 22:47:16 2012 +0200
    22.2 +++ b/src/HOL/Divides.thy	Wed Aug 22 22:55:41 2012 +0200
    22.3 @@ -7,9 +7,10 @@
    22.4  
    22.5  theory Divides
    22.6  imports Nat_Transfer
    22.7 -uses "~~/src/Provers/Arith/cancel_div_mod.ML"
    22.8  begin
    22.9  
   22.10 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
   22.11 +
   22.12  subsection {* Syntactic division operations *}
   22.13  
   22.14  class div = dvd +
    23.1 --- a/src/HOL/Extraction.thy	Wed Aug 22 22:47:16 2012 +0200
    23.2 +++ b/src/HOL/Extraction.thy	Wed Aug 22 22:55:41 2012 +0200
    23.3 @@ -6,9 +6,10 @@
    23.4  
    23.5  theory Extraction
    23.6  imports Option
    23.7 -uses "Tools/rewrite_hol_proof.ML"
    23.8  begin
    23.9  
   23.10 +ML_file "Tools/rewrite_hol_proof.ML"
   23.11 +
   23.12  subsection {* Setup *}
   23.13  
   23.14  setup {*
    24.1 --- a/src/HOL/Finite_Set.thy	Wed Aug 22 22:47:16 2012 +0200
    24.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 22 22:55:41 2012 +0200
    24.3 @@ -7,7 +7,6 @@
    24.4  
    24.5  theory Finite_Set
    24.6  imports Option Power
    24.7 -uses ("Tools/set_comprehension_pointfree.ML")
    24.8  begin
    24.9  
   24.10  subsection {* Predicate for finite sets *}
   24.11 @@ -18,7 +17,7 @@
   24.12    | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
   24.13  
   24.14  (* FIXME: move to Set theory *)
   24.15 -use "Tools/set_comprehension_pointfree.ML"
   24.16 +ML_file "Tools/set_comprehension_pointfree.ML"
   24.17  
   24.18  simproc_setup finite_Collect ("finite (Collect P)") =
   24.19    {* K Set_Comprehension_Pointfree.simproc *}
    25.1 --- a/src/HOL/Fun.thy	Wed Aug 22 22:47:16 2012 +0200
    25.2 +++ b/src/HOL/Fun.thy	Wed Aug 22 22:55:41 2012 +0200
    25.3 @@ -8,7 +8,6 @@
    25.4  theory Fun
    25.5  imports Complete_Lattices
    25.6  keywords "enriched_type" :: thy_goal
    25.7 -uses ("Tools/enriched_type.ML")
    25.8  begin
    25.9  
   25.10  lemma apply_inverse:
   25.11 @@ -801,7 +800,7 @@
   25.12  
   25.13  subsubsection {* Functorial structure of types *}
   25.14  
   25.15 -use "Tools/enriched_type.ML"
   25.16 +ML_file "Tools/enriched_type.ML"
   25.17  
   25.18  enriched_type map_fun: map_fun
   25.19    by (simp_all add: fun_eq_iff)
    26.1 --- a/src/HOL/FunDef.thy	Wed Aug 22 22:47:16 2012 +0200
    26.2 +++ b/src/HOL/FunDef.thy	Wed Aug 22 22:55:41 2012 +0200
    26.3 @@ -7,27 +7,11 @@
    26.4  theory FunDef
    26.5  imports Partial_Function Wellfounded
    26.6  keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
    26.7 -uses
    26.8 -  "Tools/prop_logic.ML"
    26.9 -  "Tools/sat_solver.ML"
   26.10 -  ("Tools/Function/function_common.ML")
   26.11 -  ("Tools/Function/context_tree.ML")
   26.12 -  ("Tools/Function/function_core.ML")
   26.13 -  ("Tools/Function/sum_tree.ML")
   26.14 -  ("Tools/Function/mutual.ML")
   26.15 -  ("Tools/Function/pattern_split.ML")
   26.16 -  ("Tools/Function/function.ML")
   26.17 -  ("Tools/Function/relation.ML")
   26.18 -  ("Tools/Function/measure_functions.ML")
   26.19 -  ("Tools/Function/lexicographic_order.ML")
   26.20 -  ("Tools/Function/pat_completeness.ML")
   26.21 -  ("Tools/Function/fun.ML")
   26.22 -  ("Tools/Function/induction_schema.ML")
   26.23 -  ("Tools/Function/termination.ML")
   26.24 -  ("Tools/Function/scnp_solve.ML")
   26.25 -  ("Tools/Function/scnp_reconstruct.ML")
   26.26  begin
   26.27  
   26.28 +ML_file "Tools/prop_logic.ML"
   26.29 +ML_file "Tools/sat_solver.ML"
   26.30 +
   26.31  subsection {* Definitions with default value. *}
   26.32  
   26.33  definition
   26.34 @@ -101,27 +85,27 @@
   26.35    "wf R \<Longrightarrow> wfP (in_rel R)"
   26.36    by (simp add: wfP_def)
   26.37  
   26.38 -use "Tools/Function/function_common.ML"
   26.39 -use "Tools/Function/context_tree.ML"
   26.40 -use "Tools/Function/function_core.ML"
   26.41 -use "Tools/Function/sum_tree.ML"
   26.42 -use "Tools/Function/mutual.ML"
   26.43 -use "Tools/Function/pattern_split.ML"
   26.44 -use "Tools/Function/relation.ML"
   26.45 +ML_file "Tools/Function/function_common.ML"
   26.46 +ML_file "Tools/Function/context_tree.ML"
   26.47 +ML_file "Tools/Function/function_core.ML"
   26.48 +ML_file "Tools/Function/sum_tree.ML"
   26.49 +ML_file "Tools/Function/mutual.ML"
   26.50 +ML_file "Tools/Function/pattern_split.ML"
   26.51 +ML_file "Tools/Function/relation.ML"
   26.52  
   26.53  method_setup relation = {*
   26.54    Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
   26.55  *} "prove termination using a user-specified wellfounded relation"
   26.56  
   26.57 -use "Tools/Function/function.ML"
   26.58 -use "Tools/Function/pat_completeness.ML"
   26.59 +ML_file "Tools/Function/function.ML"
   26.60 +ML_file "Tools/Function/pat_completeness.ML"
   26.61  
   26.62  method_setup pat_completeness = {*
   26.63    Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
   26.64  *} "prove completeness of datatype patterns"
   26.65  
   26.66 -use "Tools/Function/fun.ML"
   26.67 -use "Tools/Function/induction_schema.ML"
   26.68 +ML_file "Tools/Function/fun.ML"
   26.69 +ML_file "Tools/Function/induction_schema.ML"
   26.70  
   26.71  method_setup induction_schema = {*
   26.72    Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
   26.73 @@ -137,7 +121,7 @@
   26.74  inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
   26.75  where is_measure_trivial: "is_measure f"
   26.76  
   26.77 -use "Tools/Function/measure_functions.ML"
   26.78 +ML_file "Tools/Function/measure_functions.ML"
   26.79  setup MeasureFunctions.setup
   26.80  
   26.81  lemma measure_size[measure_function]: "is_measure size"
   26.82 @@ -148,7 +132,7 @@
   26.83  lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
   26.84  by (rule is_measure_trivial)
   26.85  
   26.86 -use "Tools/Function/lexicographic_order.ML"
   26.87 +ML_file "Tools/Function/lexicographic_order.ML"
   26.88  
   26.89  method_setup lexicographic_order = {*
   26.90    Method.sections clasimp_modifiers >>
   26.91 @@ -323,9 +307,9 @@
   26.92  
   26.93  subsection {* Tool setup *}
   26.94  
   26.95 -use "Tools/Function/termination.ML"
   26.96 -use "Tools/Function/scnp_solve.ML"
   26.97 -use "Tools/Function/scnp_reconstruct.ML"
   26.98 +ML_file "Tools/Function/termination.ML"
   26.99 +ML_file "Tools/Function/scnp_solve.ML"
  26.100 +ML_file "Tools/Function/scnp_reconstruct.ML"
  26.101  
  26.102  setup {* ScnpReconstruct.setup *}
  26.103  
    27.1 --- a/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:47:16 2012 +0200
    27.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Aug 22 22:55:41 2012 +0200
    27.3 @@ -6,8 +6,6 @@
    27.4  
    27.5  theory Groebner_Basis
    27.6  imports Semiring_Normalization
    27.7 -uses
    27.8 -  ("Tools/groebner.ML")
    27.9  begin
   27.10  
   27.11  subsection {* Groebner Bases *}
   27.12 @@ -41,7 +39,7 @@
   27.13  
   27.14  setup Algebra_Simplification.setup
   27.15  
   27.16 -use "Tools/groebner.ML"
   27.17 +ML_file "Tools/groebner.ML"
   27.18  
   27.19  method_setup algebra = {*
   27.20    let
    28.1 --- a/src/HOL/Groups.thy	Wed Aug 22 22:47:16 2012 +0200
    28.2 +++ b/src/HOL/Groups.thy	Wed Aug 22 22:55:41 2012 +0200
    28.3 @@ -6,7 +6,6 @@
    28.4  
    28.5  theory Groups
    28.6  imports Orderings
    28.7 -uses ("Tools/group_cancel.ML")
    28.8  begin
    28.9  
   28.10  subsection {* Fact collections *}
   28.11 @@ -830,7 +829,7 @@
   28.12  
   28.13  end
   28.14  
   28.15 -use "Tools/group_cancel.ML"
   28.16 +ML_file "Tools/group_cancel.ML"
   28.17  
   28.18  simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   28.19    {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
    29.1 --- a/src/HOL/HOL.thy	Wed Aug 22 22:47:16 2012 +0200
    29.2 +++ b/src/HOL/HOL.thy	Wed Aug 22 22:55:41 2012 +0200
    29.3 @@ -10,37 +10,32 @@
    29.4    "try" "solve_direct" "quickcheck"
    29.5      "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
    29.6    "quickcheck_params" :: thy_decl
    29.7 -uses
    29.8 -  ("Tools/hologic.ML")
    29.9 -  "~~/src/Tools/misc_legacy.ML"
   29.10 -  "~~/src/Tools/try.ML"
   29.11 -  "~~/src/Tools/quickcheck.ML"
   29.12 -  "~~/src/Tools/solve_direct.ML"
   29.13 -  "~~/src/Tools/IsaPlanner/zipper.ML"
   29.14 -  "~~/src/Tools/IsaPlanner/isand.ML"
   29.15 -  "~~/src/Tools/IsaPlanner/rw_tools.ML"
   29.16 -  "~~/src/Tools/IsaPlanner/rw_inst.ML"
   29.17 -  "~~/src/Provers/hypsubst.ML"
   29.18 -  "~~/src/Provers/splitter.ML"
   29.19 -  "~~/src/Provers/classical.ML"
   29.20 -  "~~/src/Provers/blast.ML"
   29.21 -  "~~/src/Provers/clasimp.ML"
   29.22 -  "~~/src/Tools/coherent.ML"
   29.23 -  "~~/src/Tools/eqsubst.ML"
   29.24 -  "~~/src/Provers/quantifier1.ML"
   29.25 -  ("Tools/simpdata.ML")
   29.26 -  "~~/src/Tools/atomize_elim.ML"
   29.27 -  "~~/src/Tools/induct.ML"
   29.28 -  "~~/src/Tools/cong_tac.ML"
   29.29 -  "~~/src/Tools/intuitionistic.ML"
   29.30 -  "~~/src/Tools/project_rule.ML"
   29.31 -  ("~~/src/Tools/induction.ML")
   29.32 -  ("~~/src/Tools/induct_tacs.ML")
   29.33 -  ("Tools/cnf_funcs.ML")
   29.34 -  "~~/src/Tools/subtyping.ML"
   29.35 -  "~~/src/Tools/case_product.ML"
   29.36  begin
   29.37  
   29.38 +ML_file "~~/src/Tools/misc_legacy.ML"
   29.39 +ML_file "~~/src/Tools/try.ML"
   29.40 +ML_file "~~/src/Tools/quickcheck.ML"
   29.41 +ML_file "~~/src/Tools/solve_direct.ML"
   29.42 +ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
   29.43 +ML_file "~~/src/Tools/IsaPlanner/isand.ML"
   29.44 +ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
   29.45 +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
   29.46 +ML_file "~~/src/Provers/hypsubst.ML"
   29.47 +ML_file "~~/src/Provers/splitter.ML"
   29.48 +ML_file "~~/src/Provers/classical.ML"
   29.49 +ML_file "~~/src/Provers/blast.ML"
   29.50 +ML_file "~~/src/Provers/clasimp.ML"
   29.51 +ML_file "~~/src/Tools/coherent.ML"
   29.52 +ML_file "~~/src/Tools/eqsubst.ML"
   29.53 +ML_file "~~/src/Provers/quantifier1.ML"
   29.54 +ML_file "~~/src/Tools/atomize_elim.ML"
   29.55 +ML_file "~~/src/Tools/induct.ML"
   29.56 +ML_file "~~/src/Tools/cong_tac.ML"
   29.57 +ML_file "~~/src/Tools/intuitionistic.ML"
   29.58 +ML_file "~~/src/Tools/project_rule.ML"
   29.59 +ML_file "~~/src/Tools/subtyping.ML"
   29.60 +ML_file "~~/src/Tools/case_product.ML"
   29.61 +
   29.62  setup {*
   29.63    Intuitionistic.method_setup @{binding iprover}
   29.64    #> Quickcheck.setup
   29.65 @@ -702,7 +697,7 @@
   29.66    and [sym] = sym not_sym
   29.67    and [Pure.elim?] = iffD1 iffD2 impE
   29.68  
   29.69 -use "Tools/hologic.ML"
   29.70 +ML_file "Tools/hologic.ML"
   29.71  
   29.72  
   29.73  subsubsection {* Atomizing meta-level connectives *}
   29.74 @@ -1193,7 +1188,7 @@
   29.75    "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   29.76    by blast
   29.77  
   29.78 -use "Tools/simpdata.ML"
   29.79 +ML_file "Tools/simpdata.ML"
   29.80  ML {* open Simpdata *}
   29.81  
   29.82  setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
   29.83 @@ -1481,7 +1476,7 @@
   29.84  )
   29.85  *}
   29.86  
   29.87 -use "~~/src/Tools/induction.ML"
   29.88 +ML_file "~~/src/Tools/induction.ML"
   29.89  
   29.90  setup {*
   29.91    Induct.setup #> Induction.setup #>
   29.92 @@ -1563,7 +1558,7 @@
   29.93  
   29.94  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
   29.95  
   29.96 -use "~~/src/Tools/induct_tacs.ML"
   29.97 +ML_file "~~/src/Tools/induct_tacs.ML"
   29.98  setup Induct_Tacs.setup
   29.99  
  29.100  
  29.101 @@ -1701,7 +1696,7 @@
  29.102  val trans = @{thm trans}
  29.103  *}
  29.104  
  29.105 -use "Tools/cnf_funcs.ML"
  29.106 +ML_file "Tools/cnf_funcs.ML"
  29.107  
  29.108  subsection {* Code generator setup *}
  29.109  
    30.1 --- a/src/HOL/HOLCF/Cpodef.thy	Wed Aug 22 22:47:16 2012 +0200
    30.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Wed Aug 22 22:55:41 2012 +0200
    30.3 @@ -7,7 +7,6 @@
    30.4  theory Cpodef
    30.5  imports Adm
    30.6  keywords "pcpodef" "cpodef" :: thy_goal
    30.7 -uses ("Tools/cpodef.ML")
    30.8  begin
    30.9  
   30.10  subsection {* Proving a subtype is a partial order *}
   30.11 @@ -268,6 +267,6 @@
   30.12  
   30.13  subsection {* HOLCF type definition package *}
   30.14  
   30.15 -use "Tools/cpodef.ML"
   30.16 +ML_file "Tools/cpodef.ML"
   30.17  
   30.18  end
    31.1 --- a/src/HOL/HOLCF/Domain.thy	Wed Aug 22 22:47:16 2012 +0200
    31.2 +++ b/src/HOL/HOLCF/Domain.thy	Wed Aug 22 22:55:41 2012 +0200
    31.3 @@ -9,11 +9,6 @@
    31.4  keywords
    31.5    "domaindef" :: thy_decl and "lazy" "unsafe" and
    31.6    "domain_isomorphism" "domain" :: thy_decl
    31.7 -uses
    31.8 -  ("Tools/domaindef.ML")
    31.9 -  ("Tools/Domain/domain_isomorphism.ML")
   31.10 -  ("Tools/Domain/domain_axioms.ML")
   31.11 -  ("Tools/Domain/domain.ML")
   31.12  begin
   31.13  
   31.14  default_sort "domain"
   31.15 @@ -155,7 +150,7 @@
   31.16    , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}) ]
   31.17  *}
   31.18  
   31.19 -use "Tools/domaindef.ML"
   31.20 +ML_file "Tools/domaindef.ML"
   31.21  
   31.22  subsection {* Isomorphic deflations *}
   31.23  
   31.24 @@ -321,9 +316,9 @@
   31.25  
   31.26  subsection {* Setting up the domain package *}
   31.27  
   31.28 -use "Tools/Domain/domain_isomorphism.ML"
   31.29 -use "Tools/Domain/domain_axioms.ML"
   31.30 -use "Tools/Domain/domain.ML"
   31.31 +ML_file "Tools/Domain/domain_isomorphism.ML"
   31.32 +ML_file "Tools/Domain/domain_axioms.ML"
   31.33 +ML_file "Tools/Domain/domain.ML"
   31.34  
   31.35  setup Domain_Isomorphism.setup
   31.36  
    32.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Wed Aug 22 22:47:16 2012 +0200
    32.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Wed Aug 22 22:55:41 2012 +0200
    32.3 @@ -6,12 +6,6 @@
    32.4  
    32.5  theory Domain_Aux
    32.6  imports Map_Functions Fixrec
    32.7 -uses
    32.8 -  ("Tools/Domain/domain_take_proofs.ML")
    32.9 -  ("Tools/cont_consts.ML")
   32.10 -  ("Tools/cont_proc.ML")
   32.11 -  ("Tools/Domain/domain_constructors.ML")
   32.12 -  ("Tools/Domain/domain_induction.ML")
   32.13  begin
   32.14  
   32.15  subsection {* Continuous isomorphisms *}
   32.16 @@ -350,11 +344,11 @@
   32.17  
   32.18  subsection {* ML setup *}
   32.19  
   32.20 -use "Tools/Domain/domain_take_proofs.ML"
   32.21 -use "Tools/cont_consts.ML"
   32.22 -use "Tools/cont_proc.ML"
   32.23 -use "Tools/Domain/domain_constructors.ML"
   32.24 -use "Tools/Domain/domain_induction.ML"
   32.25 +ML_file "Tools/Domain/domain_take_proofs.ML"
   32.26 +ML_file "Tools/cont_consts.ML"
   32.27 +ML_file "Tools/cont_proc.ML"
   32.28 +ML_file "Tools/Domain/domain_constructors.ML"
   32.29 +ML_file "Tools/Domain/domain_induction.ML"
   32.30  
   32.31  setup Domain_Take_Proofs.setup
   32.32  
    33.1 --- a/src/HOL/HOLCF/Fixrec.thy	Wed Aug 22 22:47:16 2012 +0200
    33.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Wed Aug 22 22:55:41 2012 +0200
    33.3 @@ -7,9 +7,6 @@
    33.4  theory Fixrec
    33.5  imports Plain_HOLCF
    33.6  keywords "fixrec" :: thy_decl
    33.7 -uses
    33.8 -  ("Tools/holcf_library.ML")
    33.9 -  ("Tools/fixrec.ML")
   33.10  begin
   33.11  
   33.12  subsection {* Pattern-match monad *}
   33.13 @@ -227,8 +224,8 @@
   33.14  
   33.15  subsection {* Initializing the fixrec package *}
   33.16  
   33.17 -use "Tools/holcf_library.ML"
   33.18 -use "Tools/fixrec.ML"
   33.19 +ML_file "Tools/holcf_library.ML"
   33.20 +ML_file "Tools/fixrec.ML"
   33.21  
   33.22  method_setup fixrec_simp = {*
   33.23    Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
    34.1 --- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Aug 22 22:47:16 2012 +0200
    34.2 +++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Aug 22 22:55:41 2012 +0200
    34.3 @@ -6,9 +6,10 @@
    34.4  
    34.5  theory Correctness
    34.6  imports IOA Env Impl Impl_finite
    34.7 -uses "Check.ML"
    34.8  begin
    34.9  
   34.10 +ML_file "Check.ML"
   34.11 +
   34.12  primrec reduce :: "'a list => 'a list"
   34.13  where
   34.14    reduce_Nil:  "reduce [] = []"
    35.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Aug 22 22:47:16 2012 +0200
    35.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 22 22:55:41 2012 +0200
    35.3 @@ -8,7 +8,6 @@
    35.4  theory Hilbert_Choice
    35.5  imports Nat Wellfounded Plain
    35.6  keywords "specification" "ax_specification" :: thy_goal
    35.7 -uses ("Tools/choice_specification.ML")
    35.8  begin
    35.9  
   35.10  subsection {* Hilbert's epsilon *}
   35.11 @@ -649,6 +648,6 @@
   35.12  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
   35.13    by (simp only: someI_ex)
   35.14  
   35.15 -use "Tools/choice_specification.ML"
   35.16 +ML_file "Tools/choice_specification.ML"
   35.17  
   35.18  end
    36.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 22 22:47:16 2012 +0200
    36.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Aug 22 22:55:41 2012 +0200
    36.3 @@ -10,7 +10,6 @@
    36.4  
    36.5  theory Hoare_Logic
    36.6  imports Main
    36.7 -uses ("hoare_syntax.ML") ("hoare_tac.ML")
    36.8  begin
    36.9  
   36.10  type_synonym 'a bexp = "'a set"
   36.11 @@ -54,7 +53,7 @@
   36.12   "_hoare"      :: "['a assn,'a com,'a assn] => bool"
   36.13                   ("{_} // _ // {_}" [0,55,0] 50)
   36.14  
   36.15 -use "hoare_syntax.ML"
   36.16 +ML_file "hoare_syntax.ML"
   36.17  parse_translation {* [(@{syntax_const "_hoare_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
   36.18  print_translation {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare"})] *}
   36.19  
   36.20 @@ -94,7 +93,7 @@
   36.21    by blast
   36.22  
   36.23  lemmas AbortRule = SkipRule  -- "dummy version"
   36.24 -use "hoare_tac.ML"
   36.25 +ML_file "hoare_tac.ML"
   36.26  
   36.27  method_setup vcg = {*
   36.28    Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    37.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Aug 22 22:47:16 2012 +0200
    37.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Aug 22 22:55:41 2012 +0200
    37.3 @@ -7,7 +7,6 @@
    37.4  
    37.5  theory Hoare_Logic_Abort
    37.6  imports Main
    37.7 -uses ("hoare_syntax.ML") ("hoare_tac.ML")
    37.8  begin
    37.9  
   37.10  type_synonym 'a bexp = "'a set"
   37.11 @@ -56,7 +55,7 @@
   37.12    "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
   37.13                   ("{_} // _ // {_}" [0,55,0] 50)
   37.14  
   37.15 -use "hoare_syntax.ML"
   37.16 +ML_file "hoare_syntax.ML"
   37.17  parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, Hoare_Syntax.hoare_vars_tr)] *}
   37.18  print_translation
   37.19    {* [(@{const_syntax Valid}, Hoare_Syntax.spec_tr' @{syntax_const "_hoare_abort"})] *}
   37.20 @@ -105,7 +104,7 @@
   37.21  lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}"
   37.22    by blast
   37.23  
   37.24 -use "hoare_tac.ML"
   37.25 +ML_file "hoare_tac.ML"
   37.26  
   37.27  method_setup vcg = {*
   37.28    Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    38.1 --- a/src/HOL/Import/Import_Setup.thy	Wed Aug 22 22:47:16 2012 +0200
    38.2 +++ b/src/HOL/Import/Import_Setup.thy	Wed Aug 22 22:55:41 2012 +0200
    38.3 @@ -7,12 +7,11 @@
    38.4  
    38.5  theory Import_Setup
    38.6  imports "~~/src/HOL/Parity" "~~/src/HOL/Fact"
    38.7 -keywords
    38.8 -    "import_type_map" :: thy_decl and "import_const_map" :: thy_decl and
    38.9 -    "import_file" :: thy_decl
   38.10 -uses "import_data.ML" ("import_rule.ML")
   38.11 +keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
   38.12  begin
   38.13  
   38.14 +ML_file "import_data.ML"
   38.15 +
   38.16  lemma light_ex_imp_nonempty:
   38.17    "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
   38.18    by auto
   38.19 @@ -27,7 +26,7 @@
   38.20    "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   38.21    by auto
   38.22  
   38.23 -use "import_rule.ML"
   38.24 +ML_file "import_rule.ML"
   38.25  
   38.26  end
   38.27  
    39.1 --- a/src/HOL/Inductive.thy	Wed Aug 22 22:47:16 2012 +0200
    39.2 +++ b/src/HOL/Inductive.thy	Wed Aug 22 22:55:41 2012 +0200
    39.3 @@ -11,15 +11,6 @@
    39.4    "inductive_cases" "inductive_simps" :: thy_script and "monos" and
    39.5    "rep_datatype" :: thy_goal and
    39.6    "primrec" :: thy_decl
    39.7 -uses
    39.8 -  ("Tools/inductive.ML")
    39.9 -  ("Tools/Datatype/datatype_aux.ML")
   39.10 -  ("Tools/Datatype/datatype_prop.ML")
   39.11 -  ("Tools/Datatype/datatype_data.ML")
   39.12 -  ("Tools/Datatype/datatype_case.ML")
   39.13 -  ("Tools/Datatype/rep_datatype.ML")
   39.14 -  ("Tools/Datatype/datatype_codegen.ML")
   39.15 -  ("Tools/Datatype/primrec.ML")
   39.16  begin
   39.17  
   39.18  subsection {* Least and greatest fixed points *}
   39.19 @@ -264,7 +255,7 @@
   39.20    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   39.21    Collect_mono in_mono vimage_mono
   39.22  
   39.23 -use "Tools/inductive.ML"
   39.24 +ML_file "Tools/inductive.ML"
   39.25  setup Inductive.setup
   39.26  
   39.27  theorems [mono] =
   39.28 @@ -278,13 +269,13 @@
   39.29  
   39.30  text {* Package setup. *}
   39.31  
   39.32 -use "Tools/Datatype/datatype_aux.ML"
   39.33 -use "Tools/Datatype/datatype_prop.ML"
   39.34 -use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
   39.35 -use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
   39.36 -use "Tools/Datatype/rep_datatype.ML"
   39.37 -use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
   39.38 -use "Tools/Datatype/primrec.ML"
   39.39 +ML_file "Tools/Datatype/datatype_aux.ML"
   39.40 +ML_file "Tools/Datatype/datatype_prop.ML"
   39.41 +ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
   39.42 +ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
   39.43 +ML_file "Tools/Datatype/rep_datatype.ML"
   39.44 +ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
   39.45 +ML_file "Tools/Datatype/primrec.ML"
   39.46  
   39.47  text{* Lambda-abstractions with pattern matching: *}
   39.48  
    40.1 --- a/src/HOL/Int.thy	Wed Aug 22 22:47:16 2012 +0200
    40.2 +++ b/src/HOL/Int.thy	Wed Aug 22 22:55:41 2012 +0200
    40.3 @@ -7,8 +7,6 @@
    40.4  
    40.5  theory Int
    40.6  imports Equiv_Relations Wellfounded Quotient
    40.7 -uses
    40.8 -  ("Tools/int_arith.ML")
    40.9  begin
   40.10  
   40.11  subsection {* Definition of integers as a quotient type *}
   40.12 @@ -719,7 +717,7 @@
   40.13    of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
   40.14    of_int_0 of_int_1 of_int_add of_int_mult
   40.15  
   40.16 -use "Tools/int_arith.ML"
   40.17 +ML_file "Tools/int_arith.ML"
   40.18  declaration {* K Int_Arith.setup *}
   40.19  
   40.20  simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
    41.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Wed Aug 22 22:47:16 2012 +0200
    41.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Wed Aug 22 22:55:41 2012 +0200
    41.3 @@ -8,7 +8,6 @@
    41.4  
    41.5  theory Hoare
    41.6  imports Main
    41.7 -uses ("~~/src/HOL/Hoare/hoare_tac.ML")
    41.8  begin
    41.9  
   41.10  subsection {* Abstract syntax and semantics *}
   41.11 @@ -402,7 +401,7 @@
   41.12  
   41.13  lemmas AbortRule = SkipRule  -- "dummy version"
   41.14  
   41.15 -use "~~/src/HOL/Hoare/hoare_tac.ML"
   41.16 +ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
   41.17  
   41.18  method_setup hoare = {*
   41.19    Scan.succeed (fn ctxt =>
    42.1 --- a/src/HOL/Library/Code_Prolog.thy	Wed Aug 22 22:47:16 2012 +0200
    42.2 +++ b/src/HOL/Library/Code_Prolog.thy	Wed Aug 22 22:55:41 2012 +0200
    42.3 @@ -6,9 +6,10 @@
    42.4  
    42.5  theory Code_Prolog
    42.6  imports Main
    42.7 -uses "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
    42.8  begin
    42.9  
   42.10 +ML_file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
   42.11 +
   42.12  section {* Setup for Numerals *}
   42.13  
   42.14  setup {* Predicate_Compile_Data.ignore_consts
    43.1 --- a/src/HOL/Library/Old_Recdef.thy	Wed Aug 22 22:47:16 2012 +0200
    43.2 +++ b/src/HOL/Library/Old_Recdef.thy	Wed Aug 22 22:55:41 2012 +0200
    43.3 @@ -10,17 +10,6 @@
    43.4    "recdef" "defer_recdef" :: thy_decl and
    43.5    "recdef_tc" :: thy_goal and
    43.6    "permissive" "congs" "hints"
    43.7 -uses
    43.8 -  ("~~/src/HOL/Tools/TFL/casesplit.ML")
    43.9 -  ("~~/src/HOL/Tools/TFL/utils.ML")
   43.10 -  ("~~/src/HOL/Tools/TFL/usyntax.ML")
   43.11 -  ("~~/src/HOL/Tools/TFL/dcterm.ML")
   43.12 -  ("~~/src/HOL/Tools/TFL/thms.ML")
   43.13 -  ("~~/src/HOL/Tools/TFL/rules.ML")
   43.14 -  ("~~/src/HOL/Tools/TFL/thry.ML")
   43.15 -  ("~~/src/HOL/Tools/TFL/tfl.ML")
   43.16 -  ("~~/src/HOL/Tools/TFL/post.ML")
   43.17 -  ("~~/src/HOL/Tools/recdef.ML")
   43.18  begin
   43.19  
   43.20  subsection {* Lemmas for TFL *}
   43.21 @@ -66,16 +55,16 @@
   43.22  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
   43.23    by blast
   43.24  
   43.25 -use "~~/src/HOL/Tools/TFL/casesplit.ML"
   43.26 -use "~~/src/HOL/Tools/TFL/utils.ML"
   43.27 -use "~~/src/HOL/Tools/TFL/usyntax.ML"
   43.28 -use "~~/src/HOL/Tools/TFL/dcterm.ML"
   43.29 -use "~~/src/HOL/Tools/TFL/thms.ML"
   43.30 -use "~~/src/HOL/Tools/TFL/rules.ML"
   43.31 -use "~~/src/HOL/Tools/TFL/thry.ML"
   43.32 -use "~~/src/HOL/Tools/TFL/tfl.ML"
   43.33 -use "~~/src/HOL/Tools/TFL/post.ML"
   43.34 -use "~~/src/HOL/Tools/recdef.ML"
   43.35 +ML_file "~~/src/HOL/Tools/TFL/casesplit.ML"
   43.36 +ML_file "~~/src/HOL/Tools/TFL/utils.ML"
   43.37 +ML_file "~~/src/HOL/Tools/TFL/usyntax.ML"
   43.38 +ML_file "~~/src/HOL/Tools/TFL/dcterm.ML"
   43.39 +ML_file "~~/src/HOL/Tools/TFL/thms.ML"
   43.40 +ML_file "~~/src/HOL/Tools/TFL/rules.ML"
   43.41 +ML_file "~~/src/HOL/Tools/TFL/thry.ML"
   43.42 +ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
   43.43 +ML_file "~~/src/HOL/Tools/TFL/post.ML"
   43.44 +ML_file "~~/src/HOL/Tools/recdef.ML"
   43.45  setup Recdef.setup
   43.46  
   43.47  subsection {* Rule setup *}
    44.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Aug 22 22:47:16 2012 +0200
    44.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Aug 22 22:55:41 2012 +0200
    44.3 @@ -4,9 +4,10 @@
    44.4  
    44.5  theory Predicate_Compile_Quickcheck
    44.6  imports Main Predicate_Compile_Alternative_Defs
    44.7 -uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    44.8  begin
    44.9  
   44.10 +ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
   44.11 +
   44.12  setup {* Predicate_Compile_Quickcheck.setup *}
   44.13  
   44.14  end
   44.15 \ No newline at end of file
    45.1 --- a/src/HOL/Library/Reflection.thy	Wed Aug 22 22:47:16 2012 +0200
    45.2 +++ b/src/HOL/Library/Reflection.thy	Wed Aug 22 22:55:41 2012 +0200
    45.3 @@ -6,11 +6,11 @@
    45.4  
    45.5  theory Reflection
    45.6  imports Main
    45.7 -uses
    45.8 -  "~~/src/HOL/Library/reify_data.ML"
    45.9 -  "~~/src/HOL/Library/reflection.ML"
   45.10  begin
   45.11  
   45.12 +ML_file "~~/src/HOL/Library/reify_data.ML"
   45.13 +ML_file "~~/src/HOL/Library/reflection.ML"
   45.14 +
   45.15  setup {* Reify_Data.setup *}
   45.16  
   45.17  method_setup reify = {*
    46.1 --- a/src/HOL/Library/Sum_of_Squares.thy	Wed Aug 22 22:47:16 2012 +0200
    46.2 +++ b/src/HOL/Library/Sum_of_Squares.thy	Wed Aug 22 22:55:41 2012 +0200
    46.3 @@ -8,13 +8,13 @@
    46.4  
    46.5  theory Sum_of_Squares
    46.6  imports Complex_Main
    46.7 -uses
    46.8 -  "positivstellensatz.ML"
    46.9 -  "Sum_of_Squares/sum_of_squares.ML"
   46.10 -  "Sum_of_Squares/positivstellensatz_tools.ML"
   46.11 -  "Sum_of_Squares/sos_wrapper.ML"
   46.12  begin
   46.13  
   46.14 +ML_file "positivstellensatz.ML"
   46.15 +ML_file "Sum_of_Squares/sum_of_squares.ML"
   46.16 +ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
   46.17 +ML_file "Sum_of_Squares/sos_wrapper.ML"
   46.18 +
   46.19  text {*
   46.20    Proof method sos invocations:
   46.21    \begin{itemize}
    47.1 --- a/src/HOL/Lifting.thy	Wed Aug 22 22:47:16 2012 +0200
    47.2 +++ b/src/HOL/Lifting.thy	Wed Aug 22 22:55:41 2012 +0200
    47.3 @@ -11,12 +11,6 @@
    47.4    "print_quotmaps" "print_quotients" :: diag and
    47.5    "lift_definition" :: thy_goal and
    47.6    "setup_lifting" :: thy_decl
    47.7 -uses
    47.8 -  ("Tools/Lifting/lifting_util.ML")
    47.9 -  ("Tools/Lifting/lifting_info.ML")
   47.10 -  ("Tools/Lifting/lifting_term.ML")
   47.11 -  ("Tools/Lifting/lifting_def.ML")
   47.12 -  ("Tools/Lifting/lifting_setup.ML")
   47.13  begin
   47.14  
   47.15  subsection {* Function map *}
   47.16 @@ -418,19 +412,19 @@
   47.17  
   47.18  subsection {* ML setup *}
   47.19  
   47.20 -use "Tools/Lifting/lifting_util.ML"
   47.21 +ML_file "Tools/Lifting/lifting_util.ML"
   47.22  
   47.23 -use "Tools/Lifting/lifting_info.ML"
   47.24 +ML_file "Tools/Lifting/lifting_info.ML"
   47.25  setup Lifting_Info.setup
   47.26  
   47.27  declare fun_quotient[quot_map]
   47.28  lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
   47.29  
   47.30 -use "Tools/Lifting/lifting_term.ML"
   47.31 +ML_file "Tools/Lifting/lifting_term.ML"
   47.32  
   47.33 -use "Tools/Lifting/lifting_def.ML"
   47.34 +ML_file "Tools/Lifting/lifting_def.ML"
   47.35  
   47.36 -use "Tools/Lifting/lifting_setup.ML"
   47.37 +ML_file "Tools/Lifting/lifting_setup.ML"
   47.38  
   47.39  hide_const (open) invariant
   47.40  
    48.1 --- a/src/HOL/List.thy	Wed Aug 22 22:47:16 2012 +0200
    48.2 +++ b/src/HOL/List.thy	Wed Aug 22 22:55:41 2012 +0200
    48.3 @@ -6,9 +6,6 @@
    48.4  
    48.5  theory List
    48.6  imports Plain Presburger Code_Numeral Quotient ATP
    48.7 -uses
    48.8 -  ("Tools/list_code.ML")
    48.9 -  ("Tools/list_to_set_comprehension.ML")
   48.10  begin
   48.11  
   48.12  datatype 'a list =
   48.13 @@ -485,7 +482,7 @@
   48.14  *)
   48.15  
   48.16  
   48.17 -use "Tools/list_to_set_comprehension.ML"
   48.18 +ML_file "Tools/list_to_set_comprehension.ML"
   48.19  
   48.20  simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}
   48.21  
   48.22 @@ -5522,7 +5519,7 @@
   48.23  
   48.24  subsubsection {* Pretty lists *}
   48.25  
   48.26 -use "Tools/list_code.ML"
   48.27 +ML_file "Tools/list_code.ML"
   48.28  
   48.29  code_type list
   48.30    (SML "_ list")
    49.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Aug 22 22:47:16 2012 +0200
    49.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Aug 22 22:55:41 2012 +0200
    49.3 @@ -6,9 +6,10 @@
    49.4  
    49.5  theory ComputeFloat
    49.6  imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
    49.7 -uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    49.8  begin
    49.9  
   49.10 +ML_file "~~/src/Tools/float.ML"
   49.11 +
   49.12  definition int_of_real :: "real \<Rightarrow> int"
   49.13    where "int_of_real x = (SOME y. real y = x)"
   49.14  
   49.15 @@ -238,6 +239,6 @@
   49.16  lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
   49.17    nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
   49.18  
   49.19 -use "~~/src/HOL/Tools/float_arith.ML"
   49.20 +ML_file "~~/src/HOL/Tools/float_arith.ML"
   49.21  
   49.22  end
    50.1 --- a/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Wed Aug 22 22:47:16 2012 +0200
    50.2 +++ b/src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy	Wed Aug 22 22:55:41 2012 +0200
    50.3 @@ -5,7 +5,15 @@
    50.4  *)
    50.5  
    50.6  theory Compute_Oracle imports HOL
    50.7 -uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
    50.8  begin
    50.9  
   50.10 +ML_file "am.ML"
   50.11 +ML_file "am_compiler.ML"
   50.12 +ML_file "am_interpreter.ML"
   50.13 +ML_file "am_ghc.ML"
   50.14 +ML_file "am_sml.ML"
   50.15 +ML_file "report.ML"
   50.16 +ML_file "compute.ML"
   50.17 +ML_file "linker.ML"
   50.18 +
   50.19  end
   50.20 \ No newline at end of file
    51.1 --- a/src/HOL/Matrix_LP/Cplex.thy	Wed Aug 22 22:47:16 2012 +0200
    51.2 +++ b/src/HOL/Matrix_LP/Cplex.thy	Wed Aug 22 22:55:41 2012 +0200
    51.3 @@ -4,10 +4,13 @@
    51.4  
    51.5  theory Cplex 
    51.6  imports SparseMatrix LP ComputeFloat ComputeNumeral
    51.7 -uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
    51.8 -  "fspmlp.ML" ("matrixlp.ML")
    51.9  begin
   51.10  
   51.11 +ML_file "Cplex_tools.ML"
   51.12 +ML_file "CplexMatrixConverter.ML"
   51.13 +ML_file "FloatSparseMatrixBuilder.ML"
   51.14 +ML_file "fspmlp.ML"
   51.15 +
   51.16  lemma spm_mult_le_dual_prts: 
   51.17    assumes
   51.18    "sorted_sparse_matrix A1"
   51.19 @@ -61,7 +64,7 @@
   51.20    (mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
   51.21    by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
   51.22  
   51.23 -use "matrixlp.ML"
   51.24 +ML_file "matrixlp.ML"
   51.25  
   51.26  end
   51.27  
    52.1 --- a/src/HOL/Meson.thy	Wed Aug 22 22:47:16 2012 +0200
    52.2 +++ b/src/HOL/Meson.thy	Wed Aug 22 22:55:41 2012 +0200
    52.3 @@ -9,9 +9,6 @@
    52.4  
    52.5  theory Meson
    52.6  imports Datatype
    52.7 -uses ("Tools/Meson/meson.ML")
    52.8 -     ("Tools/Meson/meson_clausify.ML")
    52.9 -     ("Tools/Meson/meson_tactic.ML")
   52.10  begin
   52.11  
   52.12  subsection {* Negation Normal Form *}
   52.13 @@ -194,9 +191,9 @@
   52.14  
   52.15  subsection {* Meson package *}
   52.16  
   52.17 -use "Tools/Meson/meson.ML"
   52.18 -use "Tools/Meson/meson_clausify.ML"
   52.19 -use "Tools/Meson/meson_tactic.ML"
   52.20 +ML_file "Tools/Meson/meson.ML"
   52.21 +ML_file "Tools/Meson/meson_clausify.ML"
   52.22 +ML_file "Tools/Meson/meson_tactic.ML"
   52.23  
   52.24  setup {* Meson_Tactic.setup *}
   52.25  
    53.1 --- a/src/HOL/Metis.thy	Wed Aug 22 22:47:16 2012 +0200
    53.2 +++ b/src/HOL/Metis.thy	Wed Aug 22 22:55:41 2012 +0200
    53.3 @@ -9,13 +9,10 @@
    53.4  theory Metis
    53.5  imports ATP
    53.6  keywords "try0" :: diag
    53.7 -uses "~~/src/Tools/Metis/metis.ML"
    53.8 -     ("Tools/Metis/metis_generate.ML")
    53.9 -     ("Tools/Metis/metis_reconstruct.ML")
   53.10 -     ("Tools/Metis/metis_tactic.ML")
   53.11 -     ("Tools/try0.ML")
   53.12  begin
   53.13  
   53.14 +ML_file "~~/src/Tools/Metis/metis.ML"
   53.15 +
   53.16  subsection {* Literal selection and lambda-lifting helpers *}
   53.17  
   53.18  definition select :: "'a \<Rightarrow> 'a" where
   53.19 @@ -41,9 +38,9 @@
   53.20  
   53.21  subsection {* Metis package *}
   53.22  
   53.23 -use "Tools/Metis/metis_generate.ML"
   53.24 -use "Tools/Metis/metis_reconstruct.ML"
   53.25 -use "Tools/Metis/metis_tactic.ML"
   53.26 +ML_file "Tools/Metis/metis_generate.ML"
   53.27 +ML_file "Tools/Metis/metis_reconstruct.ML"
   53.28 +ML_file "Tools/Metis/metis_tactic.ML"
   53.29  
   53.30  setup {* Metis_Tactic.setup *}
   53.31  
   53.32 @@ -58,8 +55,7 @@
   53.33  
   53.34  subsection {* Try0 *}
   53.35  
   53.36 -use "Tools/try0.ML"
   53.37 -
   53.38 +ML_file "Tools/try0.ML"
   53.39  setup {* Try0.setup *}
   53.40  
   53.41  end
    54.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Wed Aug 22 22:47:16 2012 +0200
    54.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed Aug 22 22:55:41 2012 +0200
    54.3 @@ -4,10 +4,11 @@
    54.4  
    54.5  theory Mirabelle
    54.6  imports Sledgehammer
    54.7 -uses "Tools/mirabelle.ML"
    54.8 -     "../TPTP/sledgehammer_tactics.ML"
    54.9  begin
   54.10  
   54.11 +ML_file "Tools/mirabelle.ML"
   54.12 +ML_file "../TPTP/sledgehammer_tactics.ML"
   54.13 +
   54.14  (* no multithreading, no parallel proofs *)  (* FIXME *)
   54.15  ML {* Multithreading.max_threads := 1 *}
   54.16  ML {* Goal.parallel_proofs := 0 *}
    55.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed Aug 22 22:47:16 2012 +0200
    55.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Wed Aug 22 22:55:41 2012 +0200
    55.3 @@ -6,16 +6,16 @@
    55.4  
    55.5  theory Mirabelle_Test
    55.6  imports Main Mirabelle
    55.7 -uses
    55.8 -  "Tools/mirabelle_arith.ML"
    55.9 -  "Tools/mirabelle_metis.ML"
   55.10 -  "Tools/mirabelle_quickcheck.ML"
   55.11 -  "Tools/mirabelle_refute.ML"
   55.12 -  "Tools/mirabelle_sledgehammer.ML"
   55.13 -  "Tools/mirabelle_sledgehammer_filter.ML"
   55.14 -  "Tools/mirabelle_try0.ML"
   55.15  begin
   55.16  
   55.17 +ML_file "Tools/mirabelle_arith.ML"
   55.18 +ML_file "Tools/mirabelle_metis.ML"
   55.19 +ML_file "Tools/mirabelle_quickcheck.ML"
   55.20 +ML_file "Tools/mirabelle_refute.ML"
   55.21 +ML_file "Tools/mirabelle_sledgehammer.ML"
   55.22 +ML_file "Tools/mirabelle_sledgehammer_filter.ML"
   55.23 +ML_file "Tools/mirabelle_try0.ML"
   55.24 +
   55.25  text {*
   55.26    Only perform type-checking of the actions,
   55.27    any reasonable test would be too complicated.
    56.1 --- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Wed Aug 22 22:47:16 2012 +0200
    56.2 +++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy	Wed Aug 22 22:55:41 2012 +0200
    56.3 @@ -6,7 +6,6 @@
    56.4  
    56.5  theory Norm_Arith
    56.6  imports "~~/src/HOL/Library/Sum_of_Squares"
    56.7 -uses ("normarith.ML")
    56.8  begin
    56.9  
   56.10  lemma norm_cmul_rule_thm:
   56.11 @@ -111,7 +110,7 @@
   56.12    mult_1_left
   56.13    mult_1_right
   56.14  
   56.15 -use "normarith.ML"
   56.16 +ML_file "normarith.ML"
   56.17  
   56.18  method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   56.19  *} "prove simple linear statements about vector norms"
    57.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Wed Aug 22 22:47:16 2012 +0200
    57.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Wed Aug 22 22:55:41 2012 +0200
    57.3 @@ -2,9 +2,10 @@
    57.4  
    57.5  theory Mutabelle
    57.6  imports Main
    57.7 -uses "mutabelle.ML"
    57.8  begin
    57.9  
   57.10 +ML_file "mutabelle.ML"
   57.11 +
   57.12  ML {*
   57.13  val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
   57.14  
    58.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Wed Aug 22 22:47:16 2012 +0200
    58.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Wed Aug 22 22:55:41 2012 +0200
    58.3 @@ -9,11 +9,11 @@
    58.4    "~/repos/afp/thys/Polynomials/Polynomial"
    58.5    "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
    58.6    "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
    58.7 -uses
    58.8 -     "mutabelle.ML"
    58.9 -     "mutabelle_extra.ML"
   58.10  begin
   58.11  
   58.12 +ML_file "mutabelle.ML"
   58.13 +ML_file "mutabelle_extra.ML"
   58.14 +
   58.15  
   58.16  section {* configuration *}
   58.17  
    59.1 --- a/src/HOL/NSA/StarDef.thy	Wed Aug 22 22:47:16 2012 +0200
    59.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Aug 22 22:55:41 2012 +0200
    59.3 @@ -6,7 +6,6 @@
    59.4  
    59.5  theory StarDef
    59.6  imports Filter
    59.7 -uses ("transfer.ML")
    59.8  begin
    59.9  
   59.10  subsection {* A Free Ultrafilter over the Naturals *}
   59.11 @@ -88,7 +87,7 @@
   59.12  by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
   59.13  
   59.14  text {*Initialize transfer tactic.*}
   59.15 -use "transfer.ML"
   59.16 +ML_file "transfer.ML"
   59.17  setup Transfer_Principle.setup
   59.18  
   59.19  method_setup transfer = {*
    60.1 --- a/src/HOL/Nat.thy	Wed Aug 22 22:47:16 2012 +0200
    60.2 +++ b/src/HOL/Nat.thy	Wed Aug 22 22:55:41 2012 +0200
    60.3 @@ -9,14 +9,13 @@
    60.4  
    60.5  theory Nat
    60.6  imports Inductive Typedef Fun Fields
    60.7 -uses
    60.8 -  "~~/src/Tools/rat.ML"
    60.9 -  "Tools/arith_data.ML"
   60.10 -  ("Tools/nat_arith.ML")
   60.11 -  "~~/src/Provers/Arith/fast_lin_arith.ML"
   60.12 -  ("Tools/lin_arith.ML")
   60.13  begin
   60.14  
   60.15 +ML_file "~~/src/Tools/rat.ML"
   60.16 +ML_file "Tools/arith_data.ML"
   60.17 +ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
   60.18 +
   60.19 +
   60.20  subsection {* Type @{text ind} *}
   60.21  
   60.22  typedecl ind
   60.23 @@ -1492,7 +1491,7 @@
   60.24  
   60.25  setup Arith_Data.setup
   60.26  
   60.27 -use "Tools/nat_arith.ML"
   60.28 +ML_file "Tools/nat_arith.ML"
   60.29  
   60.30  simproc_setup nateq_cancel_sums
   60.31    ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
   60.32 @@ -1510,7 +1509,7 @@
   60.33    ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
   60.34    {* fn phi => fn ss => try Nat_Arith.cancel_diff_conv *}
   60.35  
   60.36 -use "Tools/lin_arith.ML"
   60.37 +ML_file "Tools/lin_arith.ML"
   60.38  setup {* Lin_Arith.global_setup *}
   60.39  declaration {* K Lin_Arith.setup *}
   60.40  
    61.1 --- a/src/HOL/Nat_Transfer.thy	Wed Aug 22 22:47:16 2012 +0200
    61.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Aug 22 22:55:41 2012 +0200
    61.3 @@ -5,7 +5,6 @@
    61.4  
    61.5  theory Nat_Transfer
    61.6  imports Int
    61.7 -uses ("Tools/legacy_transfer.ML")
    61.8  begin
    61.9  
   61.10  subsection {* Generic transfer machinery *}
   61.11 @@ -16,8 +15,7 @@
   61.12  lemma transfer_morphismI[intro]: "transfer_morphism f A"
   61.13    by (simp add: transfer_morphism_def)
   61.14  
   61.15 -use "Tools/legacy_transfer.ML"
   61.16 -
   61.17 +ML_file "Tools/legacy_transfer.ML"
   61.18  setup Legacy_Transfer.setup
   61.19  
   61.20  
    62.1 --- a/src/HOL/Nitpick.thy	Wed Aug 22 22:47:16 2012 +0200
    62.2 +++ b/src/HOL/Nitpick.thy	Wed Aug 22 22:55:41 2012 +0200
    62.3 @@ -10,21 +10,6 @@
    62.4  theory Nitpick
    62.5  imports Map Quotient SAT Record
    62.6  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
    62.7 -uses ("Tools/Nitpick/kodkod.ML")
    62.8 -     ("Tools/Nitpick/kodkod_sat.ML")
    62.9 -     ("Tools/Nitpick/nitpick_util.ML")
   62.10 -     ("Tools/Nitpick/nitpick_hol.ML")
   62.11 -     ("Tools/Nitpick/nitpick_preproc.ML")
   62.12 -     ("Tools/Nitpick/nitpick_mono.ML")
   62.13 -     ("Tools/Nitpick/nitpick_scope.ML")
   62.14 -     ("Tools/Nitpick/nitpick_peephole.ML")
   62.15 -     ("Tools/Nitpick/nitpick_rep.ML")
   62.16 -     ("Tools/Nitpick/nitpick_nut.ML")
   62.17 -     ("Tools/Nitpick/nitpick_kodkod.ML")
   62.18 -     ("Tools/Nitpick/nitpick_model.ML")
   62.19 -     ("Tools/Nitpick/nitpick.ML")
   62.20 -     ("Tools/Nitpick/nitpick_isar.ML")
   62.21 -     ("Tools/Nitpick/nitpick_tests.ML")
   62.22  begin
   62.23  
   62.24  typedecl bisim_iterator
   62.25 @@ -212,21 +197,21 @@
   62.26  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
   62.27  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
   62.28  
   62.29 -use "Tools/Nitpick/kodkod.ML"
   62.30 -use "Tools/Nitpick/kodkod_sat.ML"
   62.31 -use "Tools/Nitpick/nitpick_util.ML"
   62.32 -use "Tools/Nitpick/nitpick_hol.ML"
   62.33 -use "Tools/Nitpick/nitpick_mono.ML"
   62.34 -use "Tools/Nitpick/nitpick_preproc.ML"
   62.35 -use "Tools/Nitpick/nitpick_scope.ML"
   62.36 -use "Tools/Nitpick/nitpick_peephole.ML"
   62.37 -use "Tools/Nitpick/nitpick_rep.ML"
   62.38 -use "Tools/Nitpick/nitpick_nut.ML"
   62.39 -use "Tools/Nitpick/nitpick_kodkod.ML"
   62.40 -use "Tools/Nitpick/nitpick_model.ML"
   62.41 -use "Tools/Nitpick/nitpick.ML"
   62.42 -use "Tools/Nitpick/nitpick_isar.ML"
   62.43 -use "Tools/Nitpick/nitpick_tests.ML"
   62.44 +ML_file "Tools/Nitpick/kodkod.ML"
   62.45 +ML_file "Tools/Nitpick/kodkod_sat.ML"
   62.46 +ML_file "Tools/Nitpick/nitpick_util.ML"
   62.47 +ML_file "Tools/Nitpick/nitpick_hol.ML"
   62.48 +ML_file "Tools/Nitpick/nitpick_mono.ML"
   62.49 +ML_file "Tools/Nitpick/nitpick_preproc.ML"
   62.50 +ML_file "Tools/Nitpick/nitpick_scope.ML"
   62.51 +ML_file "Tools/Nitpick/nitpick_peephole.ML"
   62.52 +ML_file "Tools/Nitpick/nitpick_rep.ML"
   62.53 +ML_file "Tools/Nitpick/nitpick_nut.ML"
   62.54 +ML_file "Tools/Nitpick/nitpick_kodkod.ML"
   62.55 +ML_file "Tools/Nitpick/nitpick_model.ML"
   62.56 +ML_file "Tools/Nitpick/nitpick.ML"
   62.57 +ML_file "Tools/Nitpick/nitpick_isar.ML"
   62.58 +ML_file "Tools/Nitpick/nitpick_tests.ML"
   62.59  
   62.60  setup {*
   62.61    Nitpick_Isar.setup #>
    63.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Aug 22 22:47:16 2012 +0200
    63.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Wed Aug 22 22:55:41 2012 +0200
    63.3 @@ -9,9 +9,10 @@
    63.4  
    63.5  theory Mini_Nits
    63.6  imports Main
    63.7 -uses "minipick.ML"
    63.8  begin
    63.9  
   63.10 +ML_file "minipick.ML"
   63.11 +
   63.12  nitpick_params [verbose, sat_solver = MiniSat_JNI, max_threads = 1]
   63.13  
   63.14  nitpick_params [total_consts = smart]
    64.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Aug 22 22:47:16 2012 +0200
    64.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Aug 22 22:55:41 2012 +0200
    64.3 @@ -4,16 +4,6 @@
    64.4    "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
    64.5    "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
    64.6    "avoids"
    64.7 -uses
    64.8 -  ("nominal_thmdecls.ML")
    64.9 -  ("nominal_atoms.ML")
   64.10 -  ("nominal_datatype.ML")
   64.11 -  ("nominal_induct.ML") 
   64.12 -  ("nominal_permeq.ML")
   64.13 -  ("nominal_fresh_fun.ML")
   64.14 -  ("nominal_primrec.ML")
   64.15 -  ("nominal_inductive.ML")
   64.16 -  ("nominal_inductive2.ML")
   64.17  begin
   64.18  
   64.19  section {* Permutations *}
   64.20 @@ -3562,7 +3552,7 @@
   64.21  
   64.22  (*******************************************************)
   64.23  (* Setup of the theorem attributes eqvt and eqvt_force *)
   64.24 -use "nominal_thmdecls.ML"
   64.25 +ML_file "nominal_thmdecls.ML"
   64.26  setup "NominalThmDecls.setup"
   64.27  
   64.28  lemmas [eqvt] = 
   64.29 @@ -3598,11 +3588,11 @@
   64.30  (***************************************)
   64.31  (* setup for the individial atom-kinds *)
   64.32  (* and nominal datatypes               *)
   64.33 -use "nominal_atoms.ML"
   64.34 +ML_file "nominal_atoms.ML"
   64.35  
   64.36  (************************************************************)
   64.37  (* various tactics for analysing permutations, supports etc *)
   64.38 -use "nominal_permeq.ML"
   64.39 +ML_file "nominal_permeq.ML"
   64.40  
   64.41  method_setup perm_simp =
   64.42    {* NominalPermeq.perm_simp_meth *}
   64.43 @@ -3646,7 +3636,7 @@
   64.44  
   64.45  (*****************************************************************)
   64.46  (* tactics for generating fresh names and simplifying fresh_funs *)
   64.47 -use "nominal_fresh_fun.ML"
   64.48 +ML_file "nominal_fresh_fun.ML"
   64.49  
   64.50  method_setup generate_fresh = 
   64.51    {* setup_generate_fresh *} 
   64.52 @@ -3662,20 +3652,20 @@
   64.53  lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
   64.54    using assms ..
   64.55  
   64.56 -use "nominal_datatype.ML"
   64.57 +ML_file "nominal_datatype.ML"
   64.58  
   64.59  (******************************************************)
   64.60  (* primitive recursive functions on nominal datatypes *)
   64.61 -use "nominal_primrec.ML"
   64.62 +ML_file "nominal_primrec.ML"
   64.63  
   64.64  (****************************************************)
   64.65  (* inductive definition involving nominal datatypes *)
   64.66 -use "nominal_inductive.ML"
   64.67 -use "nominal_inductive2.ML"
   64.68 +ML_file "nominal_inductive.ML"
   64.69 +ML_file "nominal_inductive2.ML"
   64.70  
   64.71  (*****************************************)
   64.72  (* setup for induction principles method *)
   64.73 -use "nominal_induct.ML"
   64.74 +ML_file "nominal_induct.ML"
   64.75  method_setup nominal_induct =
   64.76    {* NominalInduct.nominal_induct_method *}
   64.77    {* nominal induction *}
    65.1 --- a/src/HOL/Num.thy	Wed Aug 22 22:47:16 2012 +0200
    65.2 +++ b/src/HOL/Num.thy	Wed Aug 22 22:55:41 2012 +0200
    65.3 @@ -7,8 +7,6 @@
    65.4  
    65.5  theory Num
    65.6  imports Datatype
    65.7 -uses
    65.8 -  ("Tools/numeral.ML")
    65.9  begin
   65.10  
   65.11  subsection {* The @{text num} type *}
   65.12 @@ -333,7 +331,7 @@
   65.13      (@{const_syntax neg_numeral}, num_tr' "-")] end
   65.14  *}
   65.15  
   65.16 -use "Tools/numeral.ML"
   65.17 +ML_file "Tools/numeral.ML"
   65.18  
   65.19  
   65.20  subsection {* Class-specific numeral rules *}
    66.1 --- a/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:47:16 2012 +0200
    66.2 +++ b/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:55:41 2012 +0200
    66.3 @@ -4,16 +4,14 @@
    66.4  
    66.5  theory Numeral_Simprocs
    66.6  imports Divides
    66.7 -uses
    66.8 -  "~~/src/Provers/Arith/assoc_fold.ML"
    66.9 -  "~~/src/Provers/Arith/cancel_numerals.ML"
   66.10 -  "~~/src/Provers/Arith/combine_numerals.ML"
   66.11 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
   66.12 -  "~~/src/Provers/Arith/extract_common_term.ML"
   66.13 -  ("Tools/numeral_simprocs.ML")
   66.14 -  ("Tools/nat_numeral_simprocs.ML")
   66.15  begin
   66.16  
   66.17 +ML_file "~~/src/Provers/Arith/assoc_fold.ML"
   66.18 +ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
   66.19 +ML_file "~~/src/Provers/Arith/combine_numerals.ML"
   66.20 +ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
   66.21 +ML_file "~~/src/Provers/Arith/extract_common_term.ML"
   66.22 +
   66.23  lemmas semiring_norm =
   66.24    Let_def arith_simps nat_arith rel_simps
   66.25    if_False if_True
   66.26 @@ -100,7 +98,7 @@
   66.27       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
   66.28  by (simp add: nat_mult_div_cancel1)
   66.29  
   66.30 -use "Tools/numeral_simprocs.ML"
   66.31 +ML_file "Tools/numeral_simprocs.ML"
   66.32  
   66.33  simproc_setup semiring_assoc_fold
   66.34    ("(a::'a::comm_semiring_1_cancel) * b") =
   66.35 @@ -210,7 +208,7 @@
   66.36    |"(l::'a::field_inverse_zero) / (m * n)") =
   66.37    {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
   66.38  
   66.39 -use "Tools/nat_numeral_simprocs.ML"
   66.40 +ML_file "Tools/nat_numeral_simprocs.ML"
   66.41  
   66.42  simproc_setup nat_combine_numerals
   66.43    ("(i::nat) + j" | "Suc (i + j)") =
    67.1 --- a/src/HOL/Orderings.thy	Wed Aug 22 22:47:16 2012 +0200
    67.2 +++ b/src/HOL/Orderings.thy	Wed Aug 22 22:55:41 2012 +0200
    67.3 @@ -7,11 +7,11 @@
    67.4  theory Orderings
    67.5  imports HOL
    67.6  keywords "print_orders" :: diag
    67.7 -uses
    67.8 -  "~~/src/Provers/order.ML"
    67.9 -  "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
   67.10  begin
   67.11  
   67.12 +ML_file "~~/src/Provers/order.ML"
   67.13 +ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
   67.14 +
   67.15  subsection {* Syntactic orders *}
   67.16  
   67.17  class ord =
    68.1 --- a/src/HOL/Partial_Function.thy	Wed Aug 22 22:47:16 2012 +0200
    68.2 +++ b/src/HOL/Partial_Function.thy	Wed Aug 22 22:55:41 2012 +0200
    68.3 @@ -7,11 +7,10 @@
    68.4  theory Partial_Function
    68.5  imports Complete_Partial_Order Option
    68.6  keywords "partial_function" :: thy_decl
    68.7 -uses 
    68.8 -  "Tools/Function/function_lib.ML" 
    68.9 -  "Tools/Function/partial_function.ML" 
   68.10  begin
   68.11  
   68.12 +ML_file "Tools/Function/function_lib.ML"
   68.13 +ML_file "Tools/Function/partial_function.ML"
   68.14  setup Partial_Function.setup
   68.15  
   68.16  subsection {* Axiomatic setup *}
    69.1 --- a/src/HOL/Predicate_Compile.thy	Wed Aug 22 22:47:16 2012 +0200
    69.2 +++ b/src/HOL/Predicate_Compile.thy	Wed Aug 22 22:55:41 2012 +0200
    69.3 @@ -7,20 +7,20 @@
    69.4  theory Predicate_Compile
    69.5  imports Predicate New_Random_Sequence Quickcheck_Exhaustive
    69.6  keywords "code_pred" :: thy_goal and "values" :: diag
    69.7 -uses
    69.8 -  "Tools/Predicate_Compile/predicate_compile_aux.ML"
    69.9 -  "Tools/Predicate_Compile/predicate_compile_compilations.ML"
   69.10 -  "Tools/Predicate_Compile/core_data.ML"
   69.11 -  "Tools/Predicate_Compile/mode_inference.ML"
   69.12 -  "Tools/Predicate_Compile/predicate_compile_proof.ML"
   69.13 -  "Tools/Predicate_Compile/predicate_compile_core.ML"
   69.14 -  "Tools/Predicate_Compile/predicate_compile_data.ML"
   69.15 -  "Tools/Predicate_Compile/predicate_compile_fun.ML"
   69.16 -  "Tools/Predicate_Compile/predicate_compile_pred.ML"
   69.17 -  "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
   69.18 -  "Tools/Predicate_Compile/predicate_compile.ML"
   69.19  begin
   69.20  
   69.21 +ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"
   69.22 +ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
   69.23 +ML_file "Tools/Predicate_Compile/core_data.ML"
   69.24 +ML_file "Tools/Predicate_Compile/mode_inference.ML"
   69.25 +ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"
   69.26 +ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"
   69.27 +ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"
   69.28 +ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"
   69.29 +ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"
   69.30 +ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
   69.31 +ML_file "Tools/Predicate_Compile/predicate_compile.ML"
   69.32 +
   69.33  setup Predicate_Compile.setup
   69.34  
   69.35  end
    70.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Aug 22 22:47:16 2012 +0200
    70.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Wed Aug 22 22:55:41 2012 +0200
    70.3 @@ -1,8 +1,9 @@
    70.4  theory Hotel_Example_Small_Generator
    70.5  imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
    70.6 -uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    70.7  begin
    70.8  
    70.9 +ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
   70.10 +
   70.11  declare Let_def[code_pred_inline]
   70.12  
   70.13  lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    71.1 --- a/src/HOL/Presburger.thy	Wed Aug 22 22:47:16 2012 +0200
    71.2 +++ b/src/HOL/Presburger.thy	Wed Aug 22 22:55:41 2012 +0200
    71.3 @@ -6,12 +6,11 @@
    71.4  
    71.5  theory Presburger
    71.6  imports Groebner_Basis Set_Interval
    71.7 -uses
    71.8 -  "Tools/Qelim/qelim.ML"
    71.9 -  "Tools/Qelim/cooper_procedure.ML"
   71.10 -  ("Tools/Qelim/cooper.ML")
   71.11  begin
   71.12  
   71.13 +ML_file "Tools/Qelim/qelim.ML"
   71.14 +ML_file "Tools/Qelim/cooper_procedure.ML"
   71.15 +
   71.16  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
   71.17  
   71.18  lemma minf:
   71.19 @@ -386,7 +385,7 @@
   71.20    "\<lbrakk>x = x'; 0 \<le> x' \<Longrightarrow> P = P'\<rbrakk> \<Longrightarrow> (0 \<le> (x::int) \<and> P) = (0 \<le> x' \<and> P')"
   71.21    by (simp cong: conj_cong)
   71.22  
   71.23 -use "Tools/Qelim/cooper.ML"
   71.24 +ML_file "Tools/Qelim/cooper.ML"
   71.25  setup Cooper.setup
   71.26  
   71.27  method_setup presburger = {*
    72.1 --- a/src/HOL/Product_Type.thy	Wed Aug 22 22:47:16 2012 +0200
    72.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 22 22:55:41 2012 +0200
    72.3 @@ -8,9 +8,6 @@
    72.4  theory Product_Type
    72.5  imports Typedef Inductive Fun
    72.6  keywords "inductive_set" "coinductive_set" :: thy_decl
    72.7 -uses
    72.8 -  ("Tools/split_rule.ML")
    72.9 -  ("Tools/inductive_set.ML")
   72.10  begin
   72.11  
   72.12  subsection {* @{typ bool} is a datatype *}
   72.13 @@ -690,7 +687,7 @@
   72.14  lemma internal_split_conv: "internal_split c (a, b) = c a b"
   72.15    by (simp only: internal_split_def split_conv)
   72.16  
   72.17 -use "Tools/split_rule.ML"
   72.18 +ML_file "Tools/split_rule.ML"
   72.19  setup Split_Rule.setup
   72.20  
   72.21  hide_const internal_split
   72.22 @@ -1122,7 +1119,7 @@
   72.23  
   72.24  subsection {* Inductively defined sets *}
   72.25  
   72.26 -use "Tools/inductive_set.ML"
   72.27 +ML_file "Tools/inductive_set.ML"
   72.28  setup Inductive_Set.setup
   72.29  
   72.30  
    73.1 --- a/src/HOL/Prolog/HOHH.thy	Wed Aug 22 22:47:16 2012 +0200
    73.2 +++ b/src/HOL/Prolog/HOHH.thy	Wed Aug 22 22:55:41 2012 +0200
    73.3 @@ -6,9 +6,10 @@
    73.4  
    73.5  theory HOHH
    73.6  imports HOL
    73.7 -uses "prolog.ML"
    73.8  begin
    73.9  
   73.10 +ML_file "prolog.ML"
   73.11 +
   73.12  method_setup ptac =
   73.13    {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
   73.14    "basic Lambda Prolog interpreter"
    74.1 --- a/src/HOL/Quickcheck.thy	Wed Aug 22 22:47:16 2012 +0200
    74.2 +++ b/src/HOL/Quickcheck.thy	Wed Aug 22 22:55:41 2012 +0200
    74.3 @@ -4,9 +4,6 @@
    74.4  
    74.5  theory Quickcheck
    74.6  imports Random Code_Evaluation Enum
    74.7 -uses
    74.8 -  ("Tools/Quickcheck/quickcheck_common.ML")
    74.9 -  ("Tools/Quickcheck/random_generators.ML")
   74.10  begin
   74.11  
   74.12  notation fcomp (infixl "\<circ>>" 60)
   74.13 @@ -182,8 +179,8 @@
   74.14  
   74.15  subsection {* Deriving random generators for datatypes *}
   74.16  
   74.17 -use "Tools/Quickcheck/quickcheck_common.ML" 
   74.18 -use "Tools/Quickcheck/random_generators.ML"
   74.19 +ML_file "Tools/Quickcheck/quickcheck_common.ML" 
   74.20 +ML_file "Tools/Quickcheck/random_generators.ML"
   74.21  setup Random_Generators.setup
   74.22  
   74.23  
    75.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Aug 22 22:47:16 2012 +0200
    75.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Aug 22 22:55:41 2012 +0200
    75.3 @@ -5,9 +5,6 @@
    75.4  theory Quickcheck_Exhaustive
    75.5  imports Quickcheck
    75.6  keywords "quickcheck_generator" :: thy_decl
    75.7 -uses
    75.8 -  ("Tools/Quickcheck/exhaustive_generators.ML")
    75.9 -  ("Tools/Quickcheck/abstract_generators.ML")
   75.10  begin
   75.11  
   75.12  subsection {* basic operations for exhaustive generators *}
   75.13 @@ -577,7 +574,7 @@
   75.14  
   75.15  notation (output) unknown  ("?")
   75.16   
   75.17 -use "Tools/Quickcheck/exhaustive_generators.ML"
   75.18 +ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   75.19  
   75.20  setup {* Exhaustive_Generators.setup *}
   75.21  
   75.22 @@ -585,7 +582,7 @@
   75.23  
   75.24  subsection {* Defining generators for abstract types *}
   75.25  
   75.26 -use "Tools/Quickcheck/abstract_generators.ML"
   75.27 +ML_file "Tools/Quickcheck/abstract_generators.ML"
   75.28  
   75.29  hide_fact (open) orelse_def
   75.30  no_notation orelse (infixr "orelse" 55)
    76.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:47:16 2012 +0200
    76.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:55:41 2012 +0200
    76.3 @@ -5,11 +5,9 @@
    76.4  theory Quickcheck_Narrowing
    76.5  imports Quickcheck_Exhaustive
    76.6  keywords "find_unused_assms" :: diag
    76.7 -uses
    76.8 +uses  (* FIXME session files *)
    76.9    ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   76.10    ("Tools/Quickcheck/Narrowing_Engine.hs")
   76.11 -  ("Tools/Quickcheck/narrowing_generators.ML")
   76.12 -  ("Tools/Quickcheck/find_unused_assms.ML")
   76.13  begin
   76.14  
   76.15  subsection {* Counterexample generator *}
   76.16 @@ -340,7 +338,7 @@
   76.17  
   76.18  subsubsection {* Setting up the counterexample generator *}
   76.19  
   76.20 -use "Tools/Quickcheck/narrowing_generators.ML"
   76.21 +ML_file "Tools/Quickcheck/narrowing_generators.ML"
   76.22  
   76.23  setup {* Narrowing_Generators.setup *}
   76.24  
   76.25 @@ -447,7 +445,7 @@
   76.26  
   76.27  subsection {* The @{text find_unused_assms} command *}
   76.28  
   76.29 -use "Tools/Quickcheck/find_unused_assms.ML"
   76.30 +ML_file "Tools/Quickcheck/find_unused_assms.ML"
   76.31  
   76.32  subsection {* Closing up *}
   76.33  
    77.1 --- a/src/HOL/Quotient.thy	Wed Aug 22 22:47:16 2012 +0200
    77.2 +++ b/src/HOL/Quotient.thy	Wed Aug 22 22:55:41 2012 +0200
    77.3 @@ -10,12 +10,6 @@
    77.4    "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
    77.5    "quotient_type" :: thy_goal and "/" and
    77.6    "quotient_definition" :: thy_goal
    77.7 -uses
    77.8 -  ("Tools/Quotient/quotient_info.ML")
    77.9 -  ("Tools/Quotient/quotient_type.ML")
   77.10 -  ("Tools/Quotient/quotient_def.ML")
   77.11 -  ("Tools/Quotient/quotient_term.ML")
   77.12 -  ("Tools/Quotient/quotient_tacs.ML")
   77.13  begin
   77.14  
   77.15  text {*
   77.16 @@ -765,7 +759,7 @@
   77.17  
   77.18  text {* Auxiliary data for the quotient package *}
   77.19  
   77.20 -use "Tools/Quotient/quotient_info.ML"
   77.21 +ML_file "Tools/Quotient/quotient_info.ML"
   77.22  setup Quotient_Info.setup
   77.23  
   77.24  declare [[mapQ3 "fun" = (fun_rel, fun_quotient3)]]
   77.25 @@ -787,15 +781,15 @@
   77.26    vimage_id
   77.27  
   77.28  text {* Translation functions for the lifting process. *}
   77.29 -use "Tools/Quotient/quotient_term.ML"
   77.30 +ML_file "Tools/Quotient/quotient_term.ML"
   77.31  
   77.32  
   77.33  text {* Definitions of the quotient types. *}
   77.34 -use "Tools/Quotient/quotient_type.ML"
   77.35 +ML_file "Tools/Quotient/quotient_type.ML"
   77.36  
   77.37  
   77.38  text {* Definitions for quotient constants. *}
   77.39 -use "Tools/Quotient/quotient_def.ML"
   77.40 +ML_file "Tools/Quotient/quotient_def.ML"
   77.41  
   77.42  
   77.43  text {*
   77.44 @@ -820,7 +814,7 @@
   77.45  
   77.46  
   77.47  text {* Tactics for proving the lifted theorems *}
   77.48 -use "Tools/Quotient/quotient_tacs.ML"
   77.49 +ML_file "Tools/Quotient/quotient_tacs.ML"
   77.50  
   77.51  subsection {* Methods / Interface *}
   77.52  
    78.1 --- a/src/HOL/Rat.thy	Wed Aug 22 22:47:16 2012 +0200
    78.2 +++ b/src/HOL/Rat.thy	Wed Aug 22 22:55:41 2012 +0200
    78.3 @@ -6,7 +6,6 @@
    78.4  
    78.5  theory Rat
    78.6  imports GCD Archimedean_Field
    78.7 -uses ("Tools/float_syntax.ML")
    78.8  begin
    78.9  
   78.10  subsection {* Rational numbers as quotient *}
   78.11 @@ -1107,7 +1106,7 @@
   78.12  
   78.13  syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
   78.14  
   78.15 -use "Tools/float_syntax.ML"
   78.16 +ML_file "Tools/float_syntax.ML"
   78.17  setup Float_Syntax.setup
   78.18  
   78.19  text{* Test: *}
    79.1 --- a/src/HOL/Real.thy	Wed Aug 22 22:47:16 2012 +0200
    79.2 +++ b/src/HOL/Real.thy	Wed Aug 22 22:55:41 2012 +0200
    79.3 @@ -1,8 +1,8 @@
    79.4  theory Real
    79.5  imports RComplete RealVector
    79.6 -uses "Tools/SMT/smt_real.ML"
    79.7  begin
    79.8  
    79.9 -setup {* SMT_Real.setup *}
   79.10 +ML_file "Tools/SMT/smt_real.ML"
   79.11 +setup SMT_Real.setup
   79.12  
   79.13  end
    80.1 --- a/src/HOL/Record.thy	Wed Aug 22 22:47:16 2012 +0200
    80.2 +++ b/src/HOL/Record.thy	Wed Aug 22 22:55:41 2012 +0200
    80.3 @@ -11,7 +11,6 @@
    80.4  theory Record
    80.5  imports Plain Quickcheck_Narrowing
    80.6  keywords "record" :: thy_decl
    80.7 -uses ("Tools/record.ML")
    80.8  begin
    80.9  
   80.10  subsection {* Introduction *}
   80.11 @@ -461,7 +460,7 @@
   80.12  
   80.13  subsection {* Record package *}
   80.14  
   80.15 -use "Tools/record.ML" setup Record.setup
   80.16 +ML_file "Tools/record.ML" setup Record.setup
   80.17  
   80.18  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   80.19    iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
    81.1 --- a/src/HOL/Refute.thy	Wed Aug 22 22:47:16 2012 +0200
    81.2 +++ b/src/HOL/Refute.thy	Wed Aug 22 22:55:41 2012 +0200
    81.3 @@ -10,9 +10,9 @@
    81.4  theory Refute
    81.5  imports Hilbert_Choice List Sledgehammer
    81.6  keywords "refute" :: diag and "refute_params" :: thy_decl
    81.7 -uses "Tools/refute.ML"
    81.8  begin
    81.9  
   81.10 +ML_file "Tools/refute.ML"
   81.11  setup Refute.setup
   81.12  
   81.13  refute_params
    82.1 --- a/src/HOL/SAT.thy	Wed Aug 22 22:47:16 2012 +0200
    82.2 +++ b/src/HOL/SAT.thy	Wed Aug 22 22:55:41 2012 +0200
    82.3 @@ -9,10 +9,10 @@
    82.4  
    82.5  theory SAT
    82.6  imports Refute
    82.7 -uses
    82.8 -  "Tools/sat_funcs.ML"
    82.9  begin
   82.10  
   82.11 +ML_file "Tools/sat_funcs.ML"
   82.12 +
   82.13  ML {* structure sat = SATFunc(cnf) *}
   82.14  
   82.15  method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
    83.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Wed Aug 22 22:47:16 2012 +0200
    83.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Wed Aug 22 22:55:41 2012 +0200
    83.3 @@ -10,13 +10,11 @@
    83.4  keywords
    83.5    "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
    83.6    "spark_vc" :: thy_goal and "spark_status" :: diag
    83.7 -uses
    83.8 -  "Tools/fdl_lexer.ML"
    83.9 -  "Tools/fdl_parser.ML"
   83.10 -  ("Tools/spark_vcs.ML")
   83.11 -  ("Tools/spark_commands.ML")
   83.12  begin
   83.13  
   83.14 +ML_file "Tools/fdl_lexer.ML"
   83.15 +ML_file "Tools/fdl_parser.ML"
   83.16 +
   83.17  text {*
   83.18  SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
   83.19  *}
   83.20 @@ -180,8 +178,8 @@
   83.21  
   83.22  text {* Load the package *}
   83.23  
   83.24 -use "Tools/spark_vcs.ML"
   83.25 -use "Tools/spark_commands.ML"
   83.26 +ML_file "Tools/spark_vcs.ML"
   83.27 +ML_file "Tools/spark_commands.ML"
   83.28  
   83.29  setup SPARK_Commands.setup
   83.30  
    84.1 --- a/src/HOL/Semiring_Normalization.thy	Wed Aug 22 22:47:16 2012 +0200
    84.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed Aug 22 22:55:41 2012 +0200
    84.3 @@ -6,10 +6,10 @@
    84.4  
    84.5  theory Semiring_Normalization
    84.6  imports Numeral_Simprocs Nat_Transfer
    84.7 -uses
    84.8 -  "Tools/semiring_normalizer.ML"
    84.9  begin
   84.10  
   84.11 +ML_file "Tools/semiring_normalizer.ML"
   84.12 +
   84.13  text {* Prelude *}
   84.14  
   84.15  class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel +
    85.1 --- a/src/HOL/Sledgehammer.thy	Wed Aug 22 22:47:16 2012 +0200
    85.2 +++ b/src/HOL/Sledgehammer.thy	Wed Aug 22 22:55:41 2012 +0200
    85.3 @@ -9,17 +9,18 @@
    85.4  theory Sledgehammer
    85.5  imports ATP SMT
    85.6  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
    85.7 -uses "Tools/Sledgehammer/async_manager.ML"
    85.8 -     "Tools/Sledgehammer/sledgehammer_util.ML"
    85.9 -     "Tools/Sledgehammer/sledgehammer_fact.ML"
   85.10 -     "Tools/Sledgehammer/sledgehammer_provers.ML"
   85.11 -     "Tools/Sledgehammer/sledgehammer_minimize.ML"
   85.12 -     "Tools/Sledgehammer/sledgehammer_mepo.ML"
   85.13 -     "Tools/Sledgehammer/sledgehammer_mash.ML"
   85.14 -     "Tools/Sledgehammer/sledgehammer_run.ML"
   85.15 -     "Tools/Sledgehammer/sledgehammer_isar.ML"
   85.16  begin
   85.17  
   85.18 +ML_file "Tools/Sledgehammer/async_manager.ML"
   85.19 +ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
   85.20 +ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
   85.21 +ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
   85.22 +ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
   85.23 +ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
   85.24 +ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
   85.25 +ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
   85.26 +ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
   85.27 +
   85.28  setup {* Sledgehammer_Isar.setup *}
   85.29  
   85.30  end
    86.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Aug 22 22:47:16 2012 +0200
    86.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Aug 22 22:55:41 2012 +0200
    86.3 @@ -6,7 +6,6 @@
    86.4  
    86.5  theory DistinctTreeProver 
    86.6  imports Main
    86.7 -uses ("distinct_tree_prover.ML")
    86.8  begin
    86.9  
   86.10  text {* A state space manages a set of (abstract) names and assumes
   86.11 @@ -631,7 +630,7 @@
   86.12  text {* Now we have all the theorems in place that are needed for the
   86.13  certificate generating ML functions. *}
   86.14  
   86.15 -use "distinct_tree_prover.ML"
   86.16 +ML_file "distinct_tree_prover.ML"
   86.17  
   86.18  (* Uncomment for profiling or debugging *)
   86.19  (*
    87.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Wed Aug 22 22:47:16 2012 +0200
    87.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Wed Aug 22 22:55:41 2012 +0200
    87.3 @@ -6,9 +6,10 @@
    87.4  
    87.5  theory StateSpaceLocale imports StateFun 
    87.6  keywords "statespace" :: thy_decl
    87.7 -uses "state_space.ML" "state_fun.ML"
    87.8  begin
    87.9  
   87.10 +ML_file "state_space.ML"
   87.11 +ML_file "state_fun.ML"
   87.12  setup StateFun.setup
   87.13  
   87.14  text {* For every type that is to be stored in a state space, an
    88.1 --- a/src/HOL/String.thy	Wed Aug 22 22:47:16 2012 +0200
    88.2 +++ b/src/HOL/String.thy	Wed Aug 22 22:55:41 2012 +0200
    88.3 @@ -4,9 +4,6 @@
    88.4  
    88.5  theory String
    88.6  imports List
    88.7 -uses
    88.8 -  ("Tools/string_syntax.ML")
    88.9 -  ("Tools/string_code.ML")
   88.10  begin
   88.11  
   88.12  subsection {* Characters *}
   88.13 @@ -79,7 +76,7 @@
   88.14  syntax
   88.15    "_String" :: "str_position => string"    ("_")
   88.16  
   88.17 -use "Tools/string_syntax.ML"
   88.18 +ML_file "Tools/string_syntax.ML"
   88.19  setup String_Syntax.setup
   88.20  
   88.21  definition chars :: string where
   88.22 @@ -188,7 +185,7 @@
   88.23  
   88.24  subsection {* Code generator *}
   88.25  
   88.26 -use "Tools/string_code.ML"
   88.27 +ML_file "Tools/string_code.ML"
   88.28  
   88.29  code_reserved SML string
   88.30  code_reserved OCaml string
    89.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Aug 22 22:47:16 2012 +0200
    89.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Aug 22 22:55:41 2012 +0200
    89.3 @@ -6,10 +6,10 @@
    89.4  
    89.5  theory ATP_Problem_Import
    89.6  imports Complex_Main TPTP_Interpret
    89.7 -uses "sledgehammer_tactics.ML"
    89.8 -     ("atp_problem_import.ML")
    89.9  begin
   89.10  
   89.11 +ML_file "sledgehammer_tactics.ML"
   89.12 +
   89.13  ML {* Proofterm.proofs := 0 *}
   89.14  
   89.15  declare [[show_consts]] (* for Refute *)
   89.16 @@ -18,7 +18,7 @@
   89.17  declare [[unify_search_bound = 60]]
   89.18  declare [[unify_trace_bound = 60]]
   89.19  
   89.20 -use "atp_problem_import.ML"
   89.21 +ML_file "atp_problem_import.ML"
   89.22  
   89.23  (*
   89.24  ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
    90.1 --- a/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Aug 22 22:47:16 2012 +0200
    90.2 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy	Wed Aug 22 22:55:41 2012 +0200
    90.3 @@ -6,9 +6,10 @@
    90.4  
    90.5  theory ATP_Theory_Export
    90.6  imports Complex_Main
    90.7 -uses "atp_theory_export.ML"
    90.8  begin
    90.9  
   90.10 +ML_file "atp_theory_export.ML"
   90.11 +
   90.12  ML {*
   90.13  open ATP_Problem
   90.14  open ATP_Theory_Export
    91.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Wed Aug 22 22:47:16 2012 +0200
    91.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Wed Aug 22 22:55:41 2012 +0200
    91.3 @@ -6,9 +6,10 @@
    91.4  
    91.5  theory MaSh_Eval
    91.6  imports Complex_Main
    91.7 -uses "mash_eval.ML"
    91.8  begin
    91.9  
   91.10 +ML_file "mash_eval.ML"
   91.11 +
   91.12  sledgehammer_params
   91.13    [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
   91.14     lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
    92.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 22 22:47:16 2012 +0200
    92.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 22 22:55:41 2012 +0200
    92.3 @@ -6,9 +6,10 @@
    92.4  
    92.5  theory MaSh_Export
    92.6  imports Complex_Main
    92.7 -uses "mash_export.ML"
    92.8  begin
    92.9  
   92.10 +ML_file "mash_export.ML"
   92.11 +
   92.12  sledgehammer_params
   92.13    [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
   92.14     lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
    93.1 --- a/src/HOL/TPTP/TPTP_Interpret.thy	Wed Aug 22 22:47:16 2012 +0200
    93.2 +++ b/src/HOL/TPTP/TPTP_Interpret.thy	Wed Aug 22 22:55:41 2012 +0200
    93.3 @@ -8,9 +8,10 @@
    93.4  theory TPTP_Interpret
    93.5  imports Main TPTP_Parser
    93.6  keywords "import_tptp" :: thy_decl
    93.7 -uses  ("TPTP_Parser/tptp_interpret.ML")
    93.8 +begin
    93.9 +
   93.10 +typedecl "ind"
   93.11  
   93.12 -begin
   93.13 -typedecl "ind"
   93.14 -use  "TPTP_Parser/tptp_interpret.ML"
   93.15 +ML_file  "TPTP_Parser/tptp_interpret.ML"
   93.16 +
   93.17  end
   93.18 \ No newline at end of file
    94.1 --- a/src/HOL/TPTP/TPTP_Parser.thy	Wed Aug 22 22:47:16 2012 +0200
    94.2 +++ b/src/HOL/TPTP/TPTP_Parser.thy	Wed Aug 22 22:55:41 2012 +0200
    94.3 @@ -6,16 +6,15 @@
    94.4  
    94.5  theory TPTP_Parser
    94.6  imports Pure
    94.7 -uses
    94.8 -  "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
    94.9 +begin
   94.10 +
   94.11 +ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
   94.12  
   94.13 -  "TPTP_Parser/tptp_syntax.ML"
   94.14 -  "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
   94.15 -  "TPTP_Parser/tptp_parser.ML"
   94.16 -  "TPTP_Parser/tptp_problem_name.ML"
   94.17 -  "TPTP_Parser/tptp_proof.ML"
   94.18 -
   94.19 -begin
   94.20 +ML_file "TPTP_Parser/tptp_syntax.ML"
   94.21 +ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
   94.22 +ML_file "TPTP_Parser/tptp_parser.ML"
   94.23 +ML_file "TPTP_Parser/tptp_problem_name.ML"
   94.24 +ML_file "TPTP_Parser/tptp_proof.ML"
   94.25  
   94.26  text {*The TPTP parser was generated using ML-Yacc, and needs the
   94.27  ML-Yacc library to operate.  This library is included with the parser,
    95.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Aug 22 22:47:16 2012 +0200
    95.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Aug 22 22:55:41 2012 +0200
    95.3 @@ -6,9 +6,10 @@
    95.4  
    95.5  theory TPTP_Parser_Example
    95.6  imports TPTP_Parser TPTP_Interpret
    95.7 -uses "sledgehammer_tactics.ML"
    95.8  begin
    95.9  
   95.10 +ML_file "sledgehammer_tactics.ML"
   95.11 +
   95.12  import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
   95.13  
   95.14  ML {*
    96.1 --- a/src/HOL/Transfer.thy	Wed Aug 22 22:47:16 2012 +0200
    96.2 +++ b/src/HOL/Transfer.thy	Wed Aug 22 22:55:41 2012 +0200
    96.3 @@ -6,7 +6,6 @@
    96.4  
    96.5  theory Transfer
    96.6  imports Plain Hilbert_Choice
    96.7 -uses ("Tools/transfer.ML")
    96.8  begin
    96.9  
   96.10  subsection {* Relator for function space *}
   96.11 @@ -96,8 +95,7 @@
   96.12    shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   96.13    using assms unfolding Rel_def fun_rel_def by fast
   96.14  
   96.15 -use "Tools/transfer.ML"
   96.16 -
   96.17 +ML_file "Tools/transfer.ML"
   96.18  setup Transfer.setup
   96.19  
   96.20  declare fun_rel_eq [relator_eq]
    97.1 --- a/src/HOL/Transitive_Closure.thy	Wed Aug 22 22:47:16 2012 +0200
    97.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Aug 22 22:55:41 2012 +0200
    97.3 @@ -7,9 +7,10 @@
    97.4  
    97.5  theory Transitive_Closure
    97.6  imports Relation
    97.7 -uses "~~/src/Provers/trancl.ML"
    97.8  begin
    97.9  
   97.10 +ML_file "~~/src/Provers/trancl.ML"
   97.11 +
   97.12  text {*
   97.13    @{text rtrancl} is reflexive/transitive closure,
   97.14    @{text trancl} is transitive closure,
    98.1 --- a/src/HOL/Typedef.thy	Wed Aug 22 22:47:16 2012 +0200
    98.2 +++ b/src/HOL/Typedef.thy	Wed Aug 22 22:55:41 2012 +0200
    98.3 @@ -7,7 +7,6 @@
    98.4  theory Typedef
    98.5  imports Set
    98.6  keywords "typedef" :: thy_goal and "morphisms"
    98.7 -uses ("Tools/typedef.ML")
    98.8  begin
    98.9  
   98.10  locale type_definition =
   98.11 @@ -109,6 +108,6 @@
   98.12  
   98.13  end
   98.14  
   98.15 -use "Tools/typedef.ML" setup Typedef.setup
   98.16 +ML_file "Tools/typedef.ML" setup Typedef.setup
   98.17  
   98.18  end
    99.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Wed Aug 22 22:47:16 2012 +0200
    99.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Aug 22 22:55:41 2012 +0200
    99.3 @@ -7,9 +7,10 @@
    99.4  
    99.5  theory UNITY_Main
    99.6  imports Detects PPROD Follows ProgressSets
    99.7 -uses "UNITY_tactics.ML"
    99.8  begin
    99.9  
   99.10 +ML_file "UNITY_tactics.ML"
   99.11 +
   99.12  method_setup safety = {*
   99.13      Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
   99.14      "for proving safety properties"
   100.1 --- a/src/HOL/Wellfounded.thy	Wed Aug 22 22:47:16 2012 +0200
   100.2 +++ b/src/HOL/Wellfounded.thy	Wed Aug 22 22:55:41 2012 +0200
   100.3 @@ -9,7 +9,6 @@
   100.4  
   100.5  theory Wellfounded
   100.6  imports Transitive_Closure
   100.7 -uses ("Tools/Function/size.ML")
   100.8  begin
   100.9  
  100.10  subsection {* Basic Definitions *}
  100.11 @@ -845,8 +844,7 @@
  100.12  
  100.13  subsection {* size of a datatype value *}
  100.14  
  100.15 -use "Tools/Function/size.ML"
  100.16 -
  100.17 +ML_file "Tools/Function/size.ML"
  100.18  setup Size.setup
  100.19  
  100.20  lemma size_bool [code]:
   101.1 --- a/src/HOL/Word/Word.thy	Wed Aug 22 22:47:16 2012 +0200
   101.2 +++ b/src/HOL/Word/Word.thy	Wed Aug 22 22:55:41 2012 +0200
   101.3 @@ -10,9 +10,6 @@
   101.4    Misc_Typedef
   101.5    "~~/src/HOL/Library/Boolean_Algebra"
   101.6    Bool_List_Representation
   101.7 -uses
   101.8 -  ("~~/src/HOL/Word/Tools/smt_word.ML")
   101.9 -  ("~~/src/HOL/Word/Tools/word_lib.ML")
  101.10  begin
  101.11  
  101.12  text {* see @{text "Examples/WordExamples.thy"} for examples *}
  101.13 @@ -4647,8 +4644,8 @@
  101.14  
  101.15  declare bin_to_bl_def [simp]
  101.16  
  101.17 -use "~~/src/HOL/Word/Tools/word_lib.ML"
  101.18 -use "~~/src/HOL/Word/Tools/smt_word.ML"
  101.19 +ML_file "~~/src/HOL/Word/Tools/word_lib.ML"
  101.20 +ML_file "~~/src/HOL/Word/Tools/smt_word.ML"
  101.21  setup {* SMT_Word.setup *}
  101.22  
  101.23  hide_const (open) Word
   102.1 --- a/src/HOL/ex/Interpretation_with_Defs.thy	Wed Aug 22 22:47:16 2012 +0200
   102.2 +++ b/src/HOL/ex/Interpretation_with_Defs.thy	Wed Aug 22 22:55:41 2012 +0200
   102.3 @@ -6,7 +6,8 @@
   102.4  
   102.5  theory Interpretation_with_Defs
   102.6  imports Pure
   102.7 -uses "~~/src/Tools/interpretation_with_defs.ML"
   102.8  begin
   102.9  
  102.10 +ML_file "~~/src/Tools/interpretation_with_defs.ML"
  102.11 +
  102.12  end
   103.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Aug 22 22:47:16 2012 +0200
   103.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Aug 22 22:55:41 2012 +0200
   103.3 @@ -9,9 +9,10 @@
   103.4  
   103.5  theory SVC_Oracle
   103.6  imports Main
   103.7 -uses "svc_funcs.ML"
   103.8  begin
   103.9  
  103.10 +ML_file "svc_funcs.ML"
  103.11 +
  103.12  consts
  103.13    iff_keep :: "[bool, bool] => bool"
  103.14    iff_unfold :: "[bool, bool] => bool"
   104.1 --- a/src/Pure/Pure.thy	Wed Aug 22 22:47:16 2012 +0200
   104.2 +++ b/src/Pure/Pure.thy	Wed Aug 22 22:55:41 2012 +0200
   104.3 @@ -85,12 +85,13 @@
   104.4    and "end" :: thy_end % "theory"
   104.5    and "realizers" "realizability" "extract_type" "extract" :: thy_decl
   104.6    and "find_theorems" "find_consts" :: diag
   104.7 -  uses
   104.8 -    "Isar/isar_syn.ML"
   104.9 -    "Tools/find_theorems.ML"
  104.10 -    "Tools/find_consts.ML"
  104.11  begin
  104.12  
  104.13 +ML_file "Isar/isar_syn.ML"
  104.14 +ML_file "Tools/find_theorems.ML"
  104.15 +ML_file "Tools/find_consts.ML"
  104.16 +
  104.17 +
  104.18  section {* Further content for the Pure theory *}
  104.19  
  104.20  subsection {* Meta-level connectives in assumptions *}
   105.1 --- a/src/Sequents/LK.thy	Wed Aug 22 22:47:16 2012 +0200
   105.2 +++ b/src/Sequents/LK.thy	Wed Aug 22 22:55:41 2012 +0200
   105.3 @@ -14,7 +14,6 @@
   105.4  
   105.5  theory LK
   105.6  imports LK0
   105.7 -uses ("simpdata.ML")
   105.8  begin
   105.9  
  105.10  axiomatization where
  105.11 @@ -215,7 +214,7 @@
  105.12    apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *})
  105.13    done
  105.14  
  105.15 -use "simpdata.ML"
  105.16 +ML_file "simpdata.ML"
  105.17  setup {* Simplifier.map_simpset_global (K LK_ss) *}
  105.18  
  105.19  
   106.1 --- a/src/Sequents/Modal0.thy	Wed Aug 22 22:47:16 2012 +0200
   106.2 +++ b/src/Sequents/Modal0.thy	Wed Aug 22 22:55:41 2012 +0200
   106.3 @@ -5,9 +5,10 @@
   106.4  
   106.5  theory Modal0
   106.6  imports LK0
   106.7 -uses "modal.ML"
   106.8  begin
   106.9  
  106.10 +ML_file "modal.ML"
  106.11 +
  106.12  consts
  106.13    box           :: "o=>o"       ("[]_" [50] 50)
  106.14    dia           :: "o=>o"       ("<>_" [50] 50)
   107.1 --- a/src/Sequents/Sequents.thy	Wed Aug 22 22:47:16 2012 +0200
   107.2 +++ b/src/Sequents/Sequents.thy	Wed Aug 22 22:55:41 2012 +0200
   107.3 @@ -7,7 +7,6 @@
   107.4  
   107.5  theory Sequents
   107.6  imports Pure
   107.7 -uses ("prover.ML")
   107.8  begin
   107.9  
  107.10  setup Pure_Thy.old_appl_syntax_setup
  107.11 @@ -142,7 +141,7 @@
  107.12  
  107.13  parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
  107.14  
  107.15 -use "prover.ML"
  107.16 +ML_file "prover.ML"
  107.17  
  107.18  end
  107.19  
   108.1 --- a/src/Tools/Code_Generator.thy	Wed Aug 22 22:47:16 2012 +0200
   108.2 +++ b/src/Tools/Code_Generator.thy	Wed Aug 22 22:55:41 2012 +0200
   108.3 @@ -12,22 +12,20 @@
   108.4      "code_const" "code_reserved" "code_include" "code_modulename"
   108.5      "code_abort" "code_monad" "code_reflect" :: thy_decl and
   108.6    "datatypes" "functions" "module_name" "file" "checking"
   108.7 -uses
   108.8 -  "~~/src/Tools/value.ML"
   108.9 -  "~~/src/Tools/cache_io.ML"
  108.10 -  "~~/src/Tools/Code/code_preproc.ML"
  108.11 -  "~~/src/Tools/Code/code_thingol.ML"
  108.12 -  "~~/src/Tools/Code/code_simp.ML"
  108.13 -  "~~/src/Tools/Code/code_printer.ML"
  108.14 -  "~~/src/Tools/Code/code_target.ML"
  108.15 -  "~~/src/Tools/Code/code_namespace.ML"
  108.16 -  "~~/src/Tools/Code/code_ml.ML"
  108.17 -  "~~/src/Tools/Code/code_haskell.ML"
  108.18 -  "~~/src/Tools/Code/code_scala.ML"
  108.19 -  ("~~/src/Tools/Code/code_runtime.ML")
  108.20 -  ("~~/src/Tools/nbe.ML")
  108.21  begin
  108.22  
  108.23 +ML_file "~~/src/Tools/value.ML"
  108.24 +ML_file "~~/src/Tools/cache_io.ML"
  108.25 +ML_file "~~/src/Tools/Code/code_preproc.ML"
  108.26 +ML_file "~~/src/Tools/Code/code_thingol.ML"
  108.27 +ML_file "~~/src/Tools/Code/code_simp.ML"
  108.28 +ML_file "~~/src/Tools/Code/code_printer.ML"
  108.29 +ML_file "~~/src/Tools/Code/code_target.ML"
  108.30 +ML_file "~~/src/Tools/Code/code_namespace.ML"
  108.31 +ML_file "~~/src/Tools/Code/code_ml.ML"
  108.32 +ML_file "~~/src/Tools/Code/code_haskell.ML"
  108.33 +ML_file "~~/src/Tools/Code/code_scala.ML"
  108.34 +
  108.35  setup {*
  108.36    Value.setup
  108.37    #> Code_Preproc.setup
  108.38 @@ -65,9 +63,8 @@
  108.39      by rule (rule holds)+
  108.40  qed  
  108.41  
  108.42 -use "~~/src/Tools/Code/code_runtime.ML"
  108.43 -use "~~/src/Tools/nbe.ML"
  108.44 -
  108.45 +ML_file "~~/src/Tools/Code/code_runtime.ML"
  108.46 +ML_file "~~/src/Tools/nbe.ML"
  108.47  setup Nbe.setup
  108.48  
  108.49  hide_const (open) holds
   109.1 --- a/src/Tools/WWW_Find/WWW_Find.thy	Wed Aug 22 22:47:16 2012 +0200
   109.2 +++ b/src/Tools/WWW_Find/WWW_Find.thy	Wed Aug 22 22:55:41 2012 +0200
   109.3 @@ -1,20 +1,20 @@
   109.4  theory WWW_Find
   109.5  imports Pure
   109.6 -uses
   109.7 -  "unicode_symbols.ML"
   109.8 -  "html_unicode.ML"
   109.9 -  "mime.ML"
  109.10 -  "http_status.ML"
  109.11 -  "http_util.ML"
  109.12 -  "xhtml.ML"
  109.13 -  "socket_util.ML"
  109.14 -  "scgi_req.ML"
  109.15 -  "scgi_server.ML"
  109.16 -  "echo.ML"
  109.17 -  "html_templates.ML"
  109.18 -  "find_theorems.ML"
  109.19 -  "yxml_find_theorems.ML"
  109.20  begin
  109.21  
  109.22 +ML_file "unicode_symbols.ML"
  109.23 +ML_file "html_unicode.ML"
  109.24 +ML_file "mime.ML"
  109.25 +ML_file "http_status.ML"
  109.26 +ML_file "http_util.ML"
  109.27 +ML_file "xhtml.ML"
  109.28 +ML_file "socket_util.ML"
  109.29 +ML_file "scgi_req.ML"
  109.30 +ML_file "scgi_server.ML"
  109.31 +ML_file "echo.ML"
  109.32 +ML_file "html_templates.ML"
  109.33 +ML_file "find_theorems.ML"
  109.34 +ML_file "yxml_find_theorems.ML"
  109.35 +
  109.36  end
  109.37  
   110.1 --- a/src/ZF/ArithSimp.thy	Wed Aug 22 22:47:16 2012 +0200
   110.2 +++ b/src/ZF/ArithSimp.thy	Wed Aug 22 22:55:41 2012 +0200
   110.3 @@ -7,11 +7,13 @@
   110.4  
   110.5  theory ArithSimp
   110.6  imports Arith
   110.7 -uses "~~/src/Provers/Arith/cancel_numerals.ML"
   110.8 -      "~~/src/Provers/Arith/combine_numerals.ML"
   110.9 -      "arith_data.ML"
  110.10  begin
  110.11  
  110.12 +ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
  110.13 +ML_file "~~/src/Provers/Arith/combine_numerals.ML"
  110.14 +ML_file "arith_data.ML"
  110.15 +
  110.16 +
  110.17  subsection{*Difference*}
  110.18  
  110.19  lemma diff_self_eq_0 [simp]: "m #- m = 0"
   111.1 --- a/src/ZF/Bin.thy	Wed Aug 22 22:47:16 2012 +0200
   111.2 +++ b/src/ZF/Bin.thy	Wed Aug 22 22:55:41 2012 +0200
   111.3 @@ -17,7 +17,6 @@
   111.4  
   111.5  theory Bin
   111.6  imports Int_ZF Datatype_ZF
   111.7 -uses ("Tools/numeral_syntax.ML")
   111.8  begin
   111.9  
  111.10  consts  bin :: i
  111.11 @@ -104,7 +103,7 @@
  111.12  syntax
  111.13    "_Int"    :: "xnum_token => i"        ("_")
  111.14  
  111.15 -use "Tools/numeral_syntax.ML"
  111.16 +ML_file "Tools/numeral_syntax.ML"
  111.17  setup Numeral_Syntax.setup
  111.18  
  111.19  
   112.1 --- a/src/ZF/Datatype_ZF.thy	Wed Aug 22 22:47:16 2012 +0200
   112.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Aug 22 22:55:41 2012 +0200
   112.3 @@ -8,9 +8,10 @@
   112.4  theory Datatype_ZF
   112.5  imports Inductive_ZF Univ QUniv
   112.6  keywords "datatype" "codatatype" :: thy_decl
   112.7 -uses "Tools/datatype_package.ML"
   112.8  begin
   112.9  
  112.10 +ML_file "Tools/datatype_package.ML"
  112.11 +
  112.12  ML {*
  112.13  (*Typechecking rules for most datatypes involving univ*)
  112.14  structure Data_Arg =
   113.1 --- a/src/ZF/Inductive_ZF.thy	Wed Aug 22 22:47:16 2012 +0200
   113.2 +++ b/src/ZF/Inductive_ZF.thy	Wed Aug 22 22:55:41 2012 +0200
   113.3 @@ -18,13 +18,6 @@
   113.4    "inductive_cases" :: thy_script and
   113.5    "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   113.6    "elimination" "induction" "case_eqns" "recursor_eqns"
   113.7 -uses
   113.8 -  ("ind_syntax.ML")
   113.9 -  ("Tools/cartprod.ML")
  113.10 -  ("Tools/ind_cases.ML")
  113.11 -  ("Tools/inductive_package.ML")
  113.12 -  ("Tools/induct_tacs.ML")
  113.13 -  ("Tools/primrec_package.ML")
  113.14  begin
  113.15  
  113.16  lemma def_swap_iff: "a == b ==> a = c \<longleftrightarrow> c = b"
  113.17 @@ -35,12 +28,12 @@
  113.18  
  113.19  lemma refl_thin: "!!P. a = a ==> P ==> P" .
  113.20  
  113.21 -use "ind_syntax.ML"
  113.22 -use "Tools/ind_cases.ML"
  113.23 -use "Tools/cartprod.ML"
  113.24 -use "Tools/inductive_package.ML"
  113.25 -use "Tools/induct_tacs.ML"
  113.26 -use "Tools/primrec_package.ML"
  113.27 +ML_file "ind_syntax.ML"
  113.28 +ML_file "Tools/ind_cases.ML"
  113.29 +ML_file "Tools/cartprod.ML"
  113.30 +ML_file "Tools/inductive_package.ML"
  113.31 +ML_file "Tools/induct_tacs.ML"
  113.32 +ML_file "Tools/primrec_package.ML"
  113.33  
  113.34  setup IndCases.setup
  113.35  setup DatatypeTactics.setup
   114.1 --- a/src/ZF/IntArith.thy	Wed Aug 22 22:47:16 2012 +0200
   114.2 +++ b/src/ZF/IntArith.thy	Wed Aug 22 22:55:41 2012 +0200
   114.3 @@ -1,6 +1,5 @@
   114.4  
   114.5  theory IntArith imports Bin
   114.6 -uses ("int_arith.ML")
   114.7  begin
   114.8  
   114.9  
  114.10 @@ -90,6 +89,6 @@
  114.11    apply (simp add: zadd_ac)
  114.12    done
  114.13  
  114.14 -use "int_arith.ML"
  114.15 +ML_file "int_arith.ML"
  114.16  
  114.17  end
   115.1 --- a/src/ZF/pair.thy	Wed Aug 22 22:47:16 2012 +0200
   115.2 +++ b/src/ZF/pair.thy	Wed Aug 22 22:55:41 2012 +0200
   115.3 @@ -6,9 +6,10 @@
   115.4  header{*Ordered Pairs*}
   115.5  
   115.6  theory pair imports upair
   115.7 -uses "simpdata.ML"
   115.8  begin
   115.9  
  115.10 +ML_file "simpdata.ML"
  115.11 +
  115.12  setup {*
  115.13    Simplifier.map_simpset_global
  115.14      (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))
   116.1 --- a/src/ZF/upair.thy	Wed Aug 22 22:47:16 2012 +0200
   116.2 +++ b/src/ZF/upair.thy	Wed Aug 22 22:55:41 2012 +0200
   116.3 @@ -14,9 +14,9 @@
   116.4  theory upair
   116.5  imports ZF
   116.6  keywords "print_tcset" :: diag
   116.7 -uses "Tools/typechk.ML"
   116.8  begin
   116.9  
  116.10 +ML_file "Tools/typechk.ML"
  116.11  setup TypeCheck.setup
  116.12  
  116.13  lemma atomize_ball [symmetric, rulify]: