132 | string_for_failure CantConnect = "Cannot connect to remote server." |
128 | string_for_failure CantConnect = "Cannot connect to remote server." |
133 | string_for_failure TimedOut = "Timed out." |
129 | string_for_failure TimedOut = "Timed out." |
134 | string_for_failure Inappropriate = |
130 | string_for_failure Inappropriate = |
135 "The problem lies outside the prover's scope." |
131 "The problem lies outside the prover's scope." |
136 | string_for_failure OutOfResources = "The prover ran out of resources." |
132 | string_for_failure OutOfResources = "The prover ran out of resources." |
137 | string_for_failure SpassTooOld = |
|
138 "Isabelle requires a more recent version of SPASS with support for the \ |
|
139 \TPTP syntax. To install it, download and extract the package \ |
|
140 \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ |
|
141 \\"spass-3.7\" directory's absolute path to " ^ |
|
142 Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/etc/components")) ^ |
|
143 " on a line of its own." |
|
144 | string_for_failure VampireTooOld = |
|
145 "Isabelle requires a more recent version of Vampire. To install it, follow \ |
|
146 \the instructions from the Sledgehammer manual (\"isabelle doc\ |
|
147 \ sledgehammer\")." |
|
148 | string_for_failure NoPerl = "Perl" ^ missing_message_tail |
133 | string_for_failure NoPerl = "Perl" ^ missing_message_tail |
149 | string_for_failure NoLibwwwPerl = |
134 | string_for_failure NoLibwwwPerl = |
150 "The Perl module \"libwww-perl\"" ^ missing_message_tail |
135 "The Perl module \"libwww-perl\"" ^ missing_message_tail |
151 | string_for_failure MalformedInput = |
136 | string_for_failure MalformedInput = |
152 "The generated problem is malformed. Please report this to the Isabelle \ |
137 "The generated problem is malformed. Please report this to the Isabelle \ |