src/HOL/Sledgehammer.thy
changeset 35867 16279c4c7a33
parent 35866 513074557e06
child 35967 b9659daa5b4b
     1.1 --- a/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:33:18 2010 +0100
     1.3 @@ -101,29 +101,10 @@
     1.4  use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
     1.5  setup Sledgehammer_Proof_Reconstruct.setup
     1.6  use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
     1.7 -
     1.8 +use "Tools/ATP_Manager/atp_manager.ML"
     1.9  use "Tools/ATP_Manager/atp_wrapper.ML"
    1.10  setup ATP_Wrapper.setup
    1.11 -use "Tools/ATP_Manager/atp_manager.ML"
    1.12  use "Tools/ATP_Manager/atp_minimal.ML"
    1.13 -
    1.14 -text {* basic provers *}
    1.15 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass *}
    1.16 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *}
    1.17 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *}
    1.18 -
    1.19 -text {* provers with stuctured output *}
    1.20 -setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *}
    1.21 -setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *}
    1.22 -
    1.23 -text {* on some problems better results *}
    1.24 -setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *}
    1.25 -
    1.26 -text {* remote provers via SystemOnTPTP *}
    1.27 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *}
    1.28 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
    1.29 -setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
    1.30 -
    1.31  use "Tools/Sledgehammer/sledgehammer_isar.ML"
    1.32  
    1.33