src/HOL/HOL.thy
changeset 48891 c0eafbd55de3
parent 48776 37cd53e69840
child 49339 d1fcb4de8349
     1.1 --- a/src/HOL/HOL.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -10,37 +10,32 @@
     1.4    "try" "solve_direct" "quickcheck"
     1.5      "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
     1.6    "quickcheck_params" :: thy_decl
     1.7 -uses
     1.8 -  ("Tools/hologic.ML")
     1.9 -  "~~/src/Tools/misc_legacy.ML"
    1.10 -  "~~/src/Tools/try.ML"
    1.11 -  "~~/src/Tools/quickcheck.ML"
    1.12 -  "~~/src/Tools/solve_direct.ML"
    1.13 -  "~~/src/Tools/IsaPlanner/zipper.ML"
    1.14 -  "~~/src/Tools/IsaPlanner/isand.ML"
    1.15 -  "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.16 -  "~~/src/Tools/IsaPlanner/rw_inst.ML"
    1.17 -  "~~/src/Provers/hypsubst.ML"
    1.18 -  "~~/src/Provers/splitter.ML"
    1.19 -  "~~/src/Provers/classical.ML"
    1.20 -  "~~/src/Provers/blast.ML"
    1.21 -  "~~/src/Provers/clasimp.ML"
    1.22 -  "~~/src/Tools/coherent.ML"
    1.23 -  "~~/src/Tools/eqsubst.ML"
    1.24 -  "~~/src/Provers/quantifier1.ML"
    1.25 -  ("Tools/simpdata.ML")
    1.26 -  "~~/src/Tools/atomize_elim.ML"
    1.27 -  "~~/src/Tools/induct.ML"
    1.28 -  "~~/src/Tools/cong_tac.ML"
    1.29 -  "~~/src/Tools/intuitionistic.ML"
    1.30 -  "~~/src/Tools/project_rule.ML"
    1.31 -  ("~~/src/Tools/induction.ML")
    1.32 -  ("~~/src/Tools/induct_tacs.ML")
    1.33 -  ("Tools/cnf_funcs.ML")
    1.34 -  "~~/src/Tools/subtyping.ML"
    1.35 -  "~~/src/Tools/case_product.ML"
    1.36  begin
    1.37  
    1.38 +ML_file "~~/src/Tools/misc_legacy.ML"
    1.39 +ML_file "~~/src/Tools/try.ML"
    1.40 +ML_file "~~/src/Tools/quickcheck.ML"
    1.41 +ML_file "~~/src/Tools/solve_direct.ML"
    1.42 +ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
    1.43 +ML_file "~~/src/Tools/IsaPlanner/isand.ML"
    1.44 +ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.45 +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
    1.46 +ML_file "~~/src/Provers/hypsubst.ML"
    1.47 +ML_file "~~/src/Provers/splitter.ML"
    1.48 +ML_file "~~/src/Provers/classical.ML"
    1.49 +ML_file "~~/src/Provers/blast.ML"
    1.50 +ML_file "~~/src/Provers/clasimp.ML"
    1.51 +ML_file "~~/src/Tools/coherent.ML"
    1.52 +ML_file "~~/src/Tools/eqsubst.ML"
    1.53 +ML_file "~~/src/Provers/quantifier1.ML"
    1.54 +ML_file "~~/src/Tools/atomize_elim.ML"
    1.55 +ML_file "~~/src/Tools/induct.ML"
    1.56 +ML_file "~~/src/Tools/cong_tac.ML"
    1.57 +ML_file "~~/src/Tools/intuitionistic.ML"
    1.58 +ML_file "~~/src/Tools/project_rule.ML"
    1.59 +ML_file "~~/src/Tools/subtyping.ML"
    1.60 +ML_file "~~/src/Tools/case_product.ML"
    1.61 +
    1.62  setup {*
    1.63    Intuitionistic.method_setup @{binding iprover}
    1.64    #> Quickcheck.setup
    1.65 @@ -702,7 +697,7 @@
    1.66    and [sym] = sym not_sym
    1.67    and [Pure.elim?] = iffD1 iffD2 impE
    1.68  
    1.69 -use "Tools/hologic.ML"
    1.70 +ML_file "Tools/hologic.ML"
    1.71  
    1.72  
    1.73  subsubsection {* Atomizing meta-level connectives *}
    1.74 @@ -1193,7 +1188,7 @@
    1.75    "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
    1.76    by blast
    1.77  
    1.78 -use "Tools/simpdata.ML"
    1.79 +ML_file "Tools/simpdata.ML"
    1.80  ML {* open Simpdata *}
    1.81  
    1.82  setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
    1.83 @@ -1481,7 +1476,7 @@
    1.84  )
    1.85  *}
    1.86  
    1.87 -use "~~/src/Tools/induction.ML"
    1.88 +ML_file "~~/src/Tools/induction.ML"
    1.89  
    1.90  setup {*
    1.91    Induct.setup #> Induction.setup #>
    1.92 @@ -1563,7 +1558,7 @@
    1.93  
    1.94  hide_const induct_forall induct_implies induct_equal induct_conj induct_true induct_false
    1.95  
    1.96 -use "~~/src/Tools/induct_tacs.ML"
    1.97 +ML_file "~~/src/Tools/induct_tacs.ML"
    1.98  setup Induct_Tacs.setup
    1.99  
   1.100  
   1.101 @@ -1701,7 +1696,7 @@
   1.102  val trans = @{thm trans}
   1.103  *}
   1.104  
   1.105 -use "Tools/cnf_funcs.ML"
   1.106 +ML_file "Tools/cnf_funcs.ML"
   1.107  
   1.108  subsection {* Code generator setup *}
   1.109