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