--- a/src/HOL/ATP_Linkup.thy Fri Oct 02 04:44:56 2009 +0200
+++ b/src/HOL/ATP_Linkup.thy Sat Oct 03 12:05:40 2009 +0200
@@ -96,29 +96,26 @@
use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
use "Tools/res_atp.ML"
+use "Tools/ATP_Manager/atp_wrapper.ML" setup AtpWrapper.setup
use "Tools/ATP_Manager/atp_manager.ML"
-use "Tools/ATP_Manager/atp_wrapper.ML"
use "Tools/ATP_Manager/atp_minimal.ML"
text {* basic provers *}
-setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
-setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *}
-setup {* AtpManager.add_prover "e" AtpWrapper.eprover *}
+setup {* AtpManager.add_prover AtpWrapper.spass *}
+setup {* AtpManager.add_prover AtpWrapper.vampire *}
+setup {* AtpManager.add_prover AtpWrapper.eprover *}
text {* provers with stuctured output *}
-setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
-setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
+setup {* AtpManager.add_prover AtpWrapper.vampire_full *}
+setup {* AtpManager.add_prover AtpWrapper.eprover_full *}
text {* on some problems better results *}
-setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
+setup {* AtpManager.add_prover AtpWrapper.spass_no_tc *}
text {* remote provers via SystemOnTPTP *}
-setup {* AtpManager.add_prover "remote_vampire"
- (AtpWrapper.remote_prover_opts 60 false "" "Vampire---9") *}
-setup {* AtpManager.add_prover "remote_spass"
- (AtpWrapper.remote_prover_opts 40 true "-x" "SPASS---") *}
-setup {* AtpManager.add_prover "remote_e"
- (AtpWrapper.remote_prover_opts 100 false "" "EP---") *}
+setup {* AtpManager.add_prover AtpWrapper.remote_vampire *}
+setup {* AtpManager.add_prover AtpWrapper.remote_spass *}
+setup {* AtpManager.add_prover AtpWrapper.remote_eprover *}