src/HOL/Sledgehammer.thy
changeset 39951 ff60a6e4edfe
parent 39947 f95834c8bb4d
child 40067 0783415ed7f0
     1.1 --- a/src/HOL/Sledgehammer.thy	Tue Oct 05 10:59:12 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Tue Oct 05 11:10:37 2010 +0200
     1.3 @@ -1,18 +1,14 @@
     1.4  (*  Title:      HOL/Sledgehammer.thy
     1.5      Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     1.6      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.7 -    Author:     Fabian Immler, TU Muenchen
     1.8      Author:     Jasmin Blanchette, TU Muenchen
     1.9  *)
    1.10  
    1.11  header {* Sledgehammer: Isabelle--ATP Linkup *}
    1.12  
    1.13  theory Sledgehammer
    1.14 -imports Plain
    1.15 -uses "Tools/ATP/atp_problem.ML"
    1.16 -     "Tools/ATP/atp_proof.ML"
    1.17 -     "Tools/ATP/atp_systems.ML"
    1.18 -     "Tools/Sledgehammer/sledgehammer_util.ML"
    1.19 +imports ATP
    1.20 +uses "Tools/Sledgehammer/sledgehammer_util.ML"
    1.21       "Tools/Sledgehammer/sledgehammer_filter.ML"
    1.22       "Tools/Sledgehammer/sledgehammer_translate.ML"
    1.23       "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
    1.24 @@ -22,8 +18,7 @@
    1.25  begin
    1.26  
    1.27  setup {*
    1.28 -  ATP_Systems.setup
    1.29 -  #> Sledgehammer.setup
    1.30 +  Sledgehammer.setup
    1.31    #> Sledgehammer_Isar.setup
    1.32  *}
    1.33