src/HOL/ATP_Linkup.thy
changeset 28592 824f8390aaa2
parent 28585 be3c44ac3e86
child 28594 ed3351ff3f1b
     1.1 --- a/src/HOL/ATP_Linkup.thy	Tue Oct 14 15:45:46 2008 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Tue Oct 14 16:01:36 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    ("Tools/res_reconstruct.ML")
     1.5    ("Tools/res_atp.ML")
     1.6    ("Tools/atp_manager.ML")
     1.7 -  ("Tools/atp_thread.ML")
     1.8 +  ("Tools/atp_wrapper.ML")
     1.9    "~~/src/Tools/Metis/metis.ML"
    1.10    ("Tools/metis_tools.ML")
    1.11  begin
    1.12 @@ -97,25 +97,25 @@
    1.13  use "Tools/res_atp.ML"
    1.14  
    1.15  use "Tools/atp_manager.ML"
    1.16 -use "Tools/atp_thread.ML"
    1.17 +use "Tools/atp_wrapper.ML"
    1.18  
    1.19  text {* basic provers *}
    1.20 -setup {* AtpManager.add_prover "spass" AtpThread.spass *}
    1.21 -setup {* AtpManager.add_prover "vampire" AtpThread.vampire *}
    1.22 -setup {* AtpManager.add_prover "e" AtpThread.eprover *}
    1.23 +setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
    1.24 +setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *}
    1.25 +setup {* AtpManager.add_prover "e" AtpWrapper.eprover *}
    1.26  
    1.27  text {* provers with stuctured output *}
    1.28 -setup {* AtpManager.add_prover "vampire_full" AtpThread.vampire_full *}
    1.29 -setup {* AtpManager.add_prover "e_full" AtpThread.eprover_full *}
    1.30 +setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
    1.31 +setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
    1.32  
    1.33  text {* on some problems better results *}
    1.34 -setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *}
    1.35 +setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_filter_opts 40 false) *}
    1.36  
    1.37  text {* remote provers via SystemOnTPTP *}
    1.38  setup {* AtpManager.add_prover "remote_vamp9"
    1.39 -  (AtpThread.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
    1.40 +  (AtpWrapper.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *}
    1.41  setup {* AtpManager.add_prover "remote_vamp10"
    1.42 -  (AtpThread.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
    1.43 +  (AtpWrapper.remote_prover "Vampire---10.0" "drakosha.pl 60") *}
    1.44  
    1.45  
    1.46  subsection {* The Metis prover *}