98 | string_for_failure SpassTooOld = |
98 | string_for_failure SpassTooOld = |
99 "Isabelle requires a more recent version of SPASS with support for the \ |
99 "Isabelle requires a more recent version of SPASS with support for the \ |
100 \TPTP syntax. To install it, download and extract the package \ |
100 \TPTP syntax. To install it, download and extract the package \ |
101 \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ |
101 \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ |
102 \\"spass-3.7\" directory's absolute path to " ^ |
102 \\"spass-3.7\" directory's absolute path to " ^ |
103 quote (Path.implode (Path.expand (Path.appends |
103 Path.print (Path.expand (Path.appends |
104 (Path.variable "ISABELLE_HOME_USER" :: |
104 (Path.variable "ISABELLE_HOME_USER" :: |
105 map Path.basic ["etc", "components"])))) ^ |
105 map Path.basic ["etc", "components"]))) ^ |
106 " on a line of its own." |
106 " on a line of its own." |
107 | string_for_failure VampireTooOld = |
107 | string_for_failure VampireTooOld = |
108 "Isabelle requires a more recent version of Vampire. To install it, follow \ |
108 "Isabelle requires a more recent version of Vampire. To install it, follow \ |
109 \the instructions from the Sledgehammer manual (\"isabelle doc\ |
109 \the instructions from the Sledgehammer manual (\"isabelle doc\ |
110 \ sledgehammer\")." |
110 \ sledgehammer\")." |