prefer ML_file over old uses;
authorwenzelm
Wed Aug 22 23:22:57 2012 +0200 (2012-08-22)
changeset 488920b2407f406e8
parent 48891 c0eafbd55de3
child 48894 e794efa84045
prefer ML_file over old uses;
src/HOL/SMT.thy
src/Tools/Adhoc_Overloading.thy
     1.1 --- a/src/HOL/SMT.thy	Wed Aug 22 22:55:41 2012 +0200
     1.2 +++ b/src/HOL/SMT.thy	Wed Aug 22 23:22:57 2012 +0200
     1.3 @@ -7,26 +7,11 @@
     1.4  theory SMT
     1.5  imports Record
     1.6  keywords "smt_status" :: diag
     1.7 -uses
     1.8 -  "Tools/SMT/smt_utils.ML"
     1.9 -  "Tools/SMT/smt_failure.ML"
    1.10 -  "Tools/SMT/smt_config.ML"
    1.11 -  ("Tools/SMT/smt_builtin.ML")
    1.12 -  ("Tools/SMT/smt_datatypes.ML")
    1.13 -  ("Tools/SMT/smt_normalize.ML")
    1.14 -  ("Tools/SMT/smt_translate.ML")
    1.15 -  ("Tools/SMT/smt_solver.ML")
    1.16 -  ("Tools/SMT/smtlib_interface.ML")
    1.17 -  ("Tools/SMT/z3_interface.ML")
    1.18 -  ("Tools/SMT/z3_proof_parser.ML")
    1.19 -  ("Tools/SMT/z3_proof_tools.ML")
    1.20 -  ("Tools/SMT/z3_proof_literals.ML")
    1.21 -  ("Tools/SMT/z3_proof_methods.ML")
    1.22 -  ("Tools/SMT/z3_proof_reconstruction.ML")
    1.23 -  ("Tools/SMT/z3_model.ML")
    1.24 -  ("Tools/SMT/smt_setup_solvers.ML")
    1.25  begin
    1.26  
    1.27 +ML_file "Tools/SMT/smt_utils.ML"
    1.28 +ML_file "Tools/SMT/smt_failure.ML"
    1.29 +ML_file "Tools/SMT/smt_config.ML"
    1.30  
    1.31  
    1.32  subsection {* Triggers for quantifier instantiation *}
    1.33 @@ -135,20 +120,20 @@
    1.34  
    1.35  subsection {* Setup *}
    1.36  
    1.37 -use "Tools/SMT/smt_builtin.ML"
    1.38 -use "Tools/SMT/smt_datatypes.ML"
    1.39 -use "Tools/SMT/smt_normalize.ML"
    1.40 -use "Tools/SMT/smt_translate.ML"
    1.41 -use "Tools/SMT/smt_solver.ML"
    1.42 -use "Tools/SMT/smtlib_interface.ML"
    1.43 -use "Tools/SMT/z3_interface.ML"
    1.44 -use "Tools/SMT/z3_proof_parser.ML"
    1.45 -use "Tools/SMT/z3_proof_tools.ML"
    1.46 -use "Tools/SMT/z3_proof_literals.ML"
    1.47 -use "Tools/SMT/z3_proof_methods.ML"
    1.48 -use "Tools/SMT/z3_proof_reconstruction.ML"
    1.49 -use "Tools/SMT/z3_model.ML"
    1.50 -use "Tools/SMT/smt_setup_solvers.ML"
    1.51 +ML_file "Tools/SMT/smt_builtin.ML"
    1.52 +ML_file "Tools/SMT/smt_datatypes.ML"
    1.53 +ML_file "Tools/SMT/smt_normalize.ML"
    1.54 +ML_file "Tools/SMT/smt_translate.ML"
    1.55 +ML_file "Tools/SMT/smt_solver.ML"
    1.56 +ML_file "Tools/SMT/smtlib_interface.ML"
    1.57 +ML_file "Tools/SMT/z3_interface.ML"
    1.58 +ML_file "Tools/SMT/z3_proof_parser.ML"
    1.59 +ML_file "Tools/SMT/z3_proof_tools.ML"
    1.60 +ML_file "Tools/SMT/z3_proof_literals.ML"
    1.61 +ML_file "Tools/SMT/z3_proof_methods.ML"
    1.62 +ML_file "Tools/SMT/z3_proof_reconstruction.ML"
    1.63 +ML_file "Tools/SMT/z3_model.ML"
    1.64 +ML_file "Tools/SMT/smt_setup_solvers.ML"
    1.65  
    1.66  setup {*
    1.67    SMT_Config.setup #>
     2.1 --- a/src/Tools/Adhoc_Overloading.thy	Wed Aug 22 22:55:41 2012 +0200
     2.2 +++ b/src/Tools/Adhoc_Overloading.thy	Wed Aug 22 23:22:57 2012 +0200
     2.3 @@ -6,9 +6,9 @@
     2.4  
     2.5  theory Adhoc_Overloading
     2.6  imports Pure
     2.7 -uses "adhoc_overloading.ML"
     2.8  begin
     2.9  
    2.10 +ML_file "adhoc_overloading.ML"
    2.11  setup Adhoc_Overloading.setup
    2.12  
    2.13  end