# HG changeset patch
# User wenzelm
# Date 1345670577 -7200
# Node ID 0b2407f406e88bfd918e2611798dae0f2cf9c445
# Parent  c0eafbd55de3fc679eb6100d4de2f3aa57a60182
prefer ML_file over old uses;

diff -r c0eafbd55de3 -r 0b2407f406e8 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Aug 22 22:55:41 2012 +0200
+++ b/src/HOL/SMT.thy	Wed Aug 22 23:22:57 2012 +0200
@@ -7,26 +7,11 @@
 theory SMT
 imports Record
 keywords "smt_status" :: diag
-uses
-  "Tools/SMT/smt_utils.ML"
-  "Tools/SMT/smt_failure.ML"
-  "Tools/SMT/smt_config.ML"
-  ("Tools/SMT/smt_builtin.ML")
-  ("Tools/SMT/smt_datatypes.ML")
-  ("Tools/SMT/smt_normalize.ML")
-  ("Tools/SMT/smt_translate.ML")
-  ("Tools/SMT/smt_solver.ML")
-  ("Tools/SMT/smtlib_interface.ML")
-  ("Tools/SMT/z3_interface.ML")
-  ("Tools/SMT/z3_proof_parser.ML")
-  ("Tools/SMT/z3_proof_tools.ML")
-  ("Tools/SMT/z3_proof_literals.ML")
-  ("Tools/SMT/z3_proof_methods.ML")
-  ("Tools/SMT/z3_proof_reconstruction.ML")
-  ("Tools/SMT/z3_model.ML")
-  ("Tools/SMT/smt_setup_solvers.ML")
 begin
 
+ML_file "Tools/SMT/smt_utils.ML"
+ML_file "Tools/SMT/smt_failure.ML"
+ML_file "Tools/SMT/smt_config.ML"
 
 
 subsection {* Triggers for quantifier instantiation *}
@@ -135,20 +120,20 @@
 
 subsection {* Setup *}
 
-use "Tools/SMT/smt_builtin.ML"
-use "Tools/SMT/smt_datatypes.ML"
-use "Tools/SMT/smt_normalize.ML"
-use "Tools/SMT/smt_translate.ML"
-use "Tools/SMT/smt_solver.ML"
-use "Tools/SMT/smtlib_interface.ML"
-use "Tools/SMT/z3_interface.ML"
-use "Tools/SMT/z3_proof_parser.ML"
-use "Tools/SMT/z3_proof_tools.ML"
-use "Tools/SMT/z3_proof_literals.ML"
-use "Tools/SMT/z3_proof_methods.ML"
-use "Tools/SMT/z3_proof_reconstruction.ML"
-use "Tools/SMT/z3_model.ML"
-use "Tools/SMT/smt_setup_solvers.ML"
+ML_file "Tools/SMT/smt_builtin.ML"
+ML_file "Tools/SMT/smt_datatypes.ML"
+ML_file "Tools/SMT/smt_normalize.ML"
+ML_file "Tools/SMT/smt_translate.ML"
+ML_file "Tools/SMT/smt_solver.ML"
+ML_file "Tools/SMT/smtlib_interface.ML"
+ML_file "Tools/SMT/z3_interface.ML"
+ML_file "Tools/SMT/z3_proof_parser.ML"
+ML_file "Tools/SMT/z3_proof_tools.ML"
+ML_file "Tools/SMT/z3_proof_literals.ML"
+ML_file "Tools/SMT/z3_proof_methods.ML"
+ML_file "Tools/SMT/z3_proof_reconstruction.ML"
+ML_file "Tools/SMT/z3_model.ML"
+ML_file "Tools/SMT/smt_setup_solvers.ML"
 
 setup {*
   SMT_Config.setup #>
diff -r c0eafbd55de3 -r 0b2407f406e8 src/Tools/Adhoc_Overloading.thy
--- a/src/Tools/Adhoc_Overloading.thy	Wed Aug 22 22:55:41 2012 +0200
+++ b/src/Tools/Adhoc_Overloading.thy	Wed Aug 22 23:22:57 2012 +0200
@@ -6,9 +6,9 @@
 
 theory Adhoc_Overloading
 imports Pure
-uses "adhoc_overloading.ML"
 begin
 
+ML_file "adhoc_overloading.ML"
 setup Adhoc_Overloading.setup
 
 end