src/HOL/Sledgehammer.thy
changeset 39947 f95834c8bb4d
parent 39946 78faa9b31202
child 39951 ff60a6e4edfe
     1.1 --- a/src/HOL/Sledgehammer.thy	Mon Oct 04 22:45:09 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Oct 04 22:51:53 2010 +0200
     1.3 @@ -9,32 +9,22 @@
     1.4  
     1.5  theory Sledgehammer
     1.6  imports Plain
     1.7 -uses
     1.8 -  ("Tools/ATP/atp_problem.ML")
     1.9 -  ("Tools/ATP/atp_proof.ML")
    1.10 -  ("Tools/ATP/atp_systems.ML")
    1.11 -  ("Tools/Sledgehammer/sledgehammer_util.ML")
    1.12 -  ("Tools/Sledgehammer/sledgehammer_filter.ML")
    1.13 -  ("Tools/Sledgehammer/sledgehammer_translate.ML")
    1.14 -  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
    1.15 -  ("Tools/Sledgehammer/sledgehammer.ML")
    1.16 -  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
    1.17 -  ("Tools/Sledgehammer/sledgehammer_isar.ML")
    1.18 +uses "Tools/ATP/atp_problem.ML"
    1.19 +     "Tools/ATP/atp_proof.ML"
    1.20 +     "Tools/ATP/atp_systems.ML"
    1.21 +     "Tools/Sledgehammer/sledgehammer_util.ML"
    1.22 +     "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.23 +     "Tools/Sledgehammer/sledgehammer_translate.ML"
    1.24 +     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    1.25 +     "Tools/Sledgehammer/sledgehammer.ML"
    1.26 +     "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.27 +     "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.28  begin
    1.29  
    1.30 -use "Tools/ATP/atp_problem.ML"
    1.31 -use "Tools/ATP/atp_proof.ML"
    1.32 -use "Tools/ATP/atp_systems.ML"
    1.33 -setup ATP_Systems.setup
    1.34 -
    1.35 -use "Tools/Sledgehammer/sledgehammer_util.ML"
    1.36 -use "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.37 -use "Tools/Sledgehammer/sledgehammer_translate.ML"
    1.38 -use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    1.39 -use "Tools/Sledgehammer/sledgehammer.ML"
    1.40 -setup Sledgehammer.setup
    1.41 -use "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.42 -use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.43 -setup Sledgehammer_Isar.setup
    1.44 +setup {*
    1.45 +  ATP_Systems.setup
    1.46 +  #> Sledgehammer.setup
    1.47 +  #> Sledgehammer_Isar.setup
    1.48 +*}
    1.49  
    1.50  end