tuning
authorblanchet
Mon Oct 04 22:51:53 2010 +0200 (2010-10-04)
changeset 39947f95834c8bb4d
parent 39946 78faa9b31202
child 39948 317010af8972
tuning
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Sledgehammer.thy
     1.1 --- a/src/HOL/Meson.thy	Mon Oct 04 22:45:09 2010 +0200
     1.2 +++ b/src/HOL/Meson.thy	Mon Oct 04 22:51:53 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4      Copyright   2001  University of Cambridge
     1.5  *)
     1.6  
     1.7 -header {* MESON Proof Procedure (Model Elimination) *}
     1.8 +header {* MESON Proof Method *}
     1.9  
    1.10  theory Meson
    1.11  imports Datatype
     2.1 --- a/src/HOL/Metis.thy	Mon Oct 04 22:45:09 2010 +0200
     2.2 +++ b/src/HOL/Metis.thy	Mon Oct 04 22:51:53 2010 +0200
     2.3 @@ -29,7 +29,6 @@
     2.4  use "Tools/Metis/metis_translate.ML"
     2.5  use "Tools/Metis/metis_reconstruct.ML"
     2.6  use "Tools/Metis/metis_tactics.ML"
     2.7 -
     2.8  setup Metis_Tactics.setup
     2.9  
    2.10  end
     3.1 --- a/src/HOL/Sledgehammer.thy	Mon Oct 04 22:45:09 2010 +0200
     3.2 +++ b/src/HOL/Sledgehammer.thy	Mon Oct 04 22:51:53 2010 +0200
     3.3 @@ -9,32 +9,22 @@
     3.4  
     3.5  theory Sledgehammer
     3.6  imports Plain
     3.7 -uses
     3.8 -  ("Tools/ATP/atp_problem.ML")
     3.9 -  ("Tools/ATP/atp_proof.ML")
    3.10 -  ("Tools/ATP/atp_systems.ML")
    3.11 -  ("Tools/Sledgehammer/sledgehammer_util.ML")
    3.12 -  ("Tools/Sledgehammer/sledgehammer_filter.ML")
    3.13 -  ("Tools/Sledgehammer/sledgehammer_translate.ML")
    3.14 -  ("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
    3.15 -  ("Tools/Sledgehammer/sledgehammer.ML")
    3.16 -  ("Tools/Sledgehammer/sledgehammer_minimize.ML")
    3.17 -  ("Tools/Sledgehammer/sledgehammer_isar.ML")
    3.18 +uses "Tools/ATP/atp_problem.ML"
    3.19 +     "Tools/ATP/atp_proof.ML"
    3.20 +     "Tools/ATP/atp_systems.ML"
    3.21 +     "Tools/Sledgehammer/sledgehammer_util.ML"
    3.22 +     "Tools/Sledgehammer/sledgehammer_filter.ML"
    3.23 +     "Tools/Sledgehammer/sledgehammer_translate.ML"
    3.24 +     "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    3.25 +     "Tools/Sledgehammer/sledgehammer.ML"
    3.26 +     "Tools/Sledgehammer/sledgehammer_minimize.ML"
    3.27 +     "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.28  begin
    3.29  
    3.30 -use "Tools/ATP/atp_problem.ML"
    3.31 -use "Tools/ATP/atp_proof.ML"
    3.32 -use "Tools/ATP/atp_systems.ML"
    3.33 -setup ATP_Systems.setup
    3.34 -
    3.35 -use "Tools/Sledgehammer/sledgehammer_util.ML"
    3.36 -use "Tools/Sledgehammer/sledgehammer_filter.ML"
    3.37 -use "Tools/Sledgehammer/sledgehammer_translate.ML"
    3.38 -use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    3.39 -use "Tools/Sledgehammer/sledgehammer.ML"
    3.40 -setup Sledgehammer.setup
    3.41 -use "Tools/Sledgehammer/sledgehammer_minimize.ML"
    3.42 -use "Tools/Sledgehammer/sledgehammer_isar.ML"
    3.43 -setup Sledgehammer_Isar.setup
    3.44 +setup {*
    3.45 +  ATP_Systems.setup
    3.46 +  #> Sledgehammer.setup
    3.47 +  #> Sledgehammer_Isar.setup
    3.48 +*}
    3.49  
    3.50  end