--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 18:44:50 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Aug 28 18:44:50 2013 +0200
@@ -25,7 +25,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- OldSPASS |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -81,7 +80,6 @@
TimedOut |
Inappropriate |
OutOfResources |
- OldSPASS |
NoPerl |
NoLibwwwPerl |
MalformedInput |
@@ -125,15 +123,6 @@
| string_of_failure Inappropriate =
"The generated problem lies outside the prover's scope."
| string_of_failure OutOfResources = "The prover ran out of resources."
- | string_of_failure OldSPASS =
- "The version of SPASS you are using is obsolete. Please upgrade to \
- \SPASS 3.8ds. To install it, download and extract the package \
- \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
- \\"spass-3.8ds\" directory's absolute path to " ^
- quote (Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"])))) ^
- " on a line of its own."
| string_of_failure NoPerl = "Perl" ^ missing_message_tail
| string_of_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail