src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/FunDef.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,27 +7,11 @@
 theory FunDef
 imports Partial_Function Wellfounded
 keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
-uses
-  "Tools/prop_logic.ML"
-  "Tools/sat_solver.ML"
-  ("Tools/Function/function_common.ML")
-  ("Tools/Function/context_tree.ML")
-  ("Tools/Function/function_core.ML")
-  ("Tools/Function/sum_tree.ML")
-  ("Tools/Function/mutual.ML")
-  ("Tools/Function/pattern_split.ML")
-  ("Tools/Function/function.ML")
-  ("Tools/Function/relation.ML")
-  ("Tools/Function/measure_functions.ML")
-  ("Tools/Function/lexicographic_order.ML")
-  ("Tools/Function/pat_completeness.ML")
-  ("Tools/Function/fun.ML")
-  ("Tools/Function/induction_schema.ML")
-  ("Tools/Function/termination.ML")
-  ("Tools/Function/scnp_solve.ML")
-  ("Tools/Function/scnp_reconstruct.ML")
 begin
 
+ML_file "Tools/prop_logic.ML"
+ML_file "Tools/sat_solver.ML"
+
 subsection {* Definitions with default value. *}
 
 definition
@@ -101,27 +85,27 @@
   "wf R \<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 *}