# HG changeset patch
# User wenzelm
# Date 1223055316 -7200
# Node ID 9912ab2992f60e96148227770d987348d2985183
# Parent  36b12b1be770b414fe84539690f8fc61c2cf6d3c
perform atp_setups here;

diff -r 36b12b1be770 -r 9912ab2992f6 src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Fri Oct 03 19:35:15 2008 +0200
+++ b/src/HOL/ATP_Linkup.thy	Fri Oct 03 19:35:16 2008 +0200
@@ -2,6 +2,7 @@
     ID:         $Id$
     Author:     Lawrence C Paulson
     Author:     Jia Meng, NICTA
+    Author:     Fabian Immler, TUM
 *)
 
 header {* The Isabelle-ATP Linkup *}
@@ -95,7 +96,19 @@
 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
 use "Tools/res_atp.ML"
 use "Tools/atp_manager.ML"
-use "Tools/atp_thread.ML" setup AtpThread.setup
+use "Tools/atp_thread.ML"
+
+text {* basic provers *}
+setup {* AtpManager.add_prover "spass" AtpThread.spass *}
+setup {* AtpManager.add_prover "vampire" AtpThread.vampire *}
+setup {* AtpManager.add_prover "e" AtpThread.eprover *}
+
+text {* provers with stuctured output *}
+setup {* AtpManager.add_prover "vampire_full" AtpThread.vampire_full *}
+setup {* AtpManager.add_prover "e_full" AtpThread.eprover_full *}
+
+text {* on some problems better results *}
+setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *}
 
 
 subsection {* The Metis prover *}