author | wenzelm |
Sat, 18 Aug 2007 13:32:18 +0200 | |
changeset 24318 | 2477286fcc7e |
parent 24317 | fef33067272b |
child 24319 | 944705cc79d2 |
--- a/src/HOL/ATP_Linkup.thy Sat Aug 18 00:22:22 2007 +0200 +++ b/src/HOL/ATP_Linkup.thy Sat Aug 18 13:32:18 2007 +0200 @@ -102,7 +102,7 @@ oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *} use "Tools/res_atp_methods.ML" -setup ResAtpMethods.ResAtps_setup +setup ResAtpMethods.setup subsection {* The Metis prover *}