src/HOL/Sledgehammer.thy
changeset 48891 c0eafbd55de3
parent 48380 d4b7c7be3116
child 49881 d9d73ebf9274
     1.1 --- a/src/HOL/Sledgehammer.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -9,17 +9,18 @@
     1.4  theory Sledgehammer
     1.5  imports ATP SMT
     1.6  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
     1.7 -uses "Tools/Sledgehammer/async_manager.ML"
     1.8 -     "Tools/Sledgehammer/sledgehammer_util.ML"
     1.9 -     "Tools/Sledgehammer/sledgehammer_fact.ML"
    1.10 -     "Tools/Sledgehammer/sledgehammer_provers.ML"
    1.11 -     "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.12 -     "Tools/Sledgehammer/sledgehammer_mepo.ML"
    1.13 -     "Tools/Sledgehammer/sledgehammer_mash.ML"
    1.14 -     "Tools/Sledgehammer/sledgehammer_run.ML"
    1.15 -     "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.16  begin
    1.17  
    1.18 +ML_file "Tools/Sledgehammer/async_manager.ML"
    1.19 +ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
    1.20 +ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
    1.21 +ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
    1.22 +ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.23 +ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
    1.24 +ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
    1.25 +ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
    1.26 +ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.27 +
    1.28  setup {* Sledgehammer_Isar.setup *}
    1.29  
    1.30  end