| changeset 55049 | 327eafb594ba |
| parent 53393 | 5278312037f8 |
| child 63167 | 0909deb8059b |
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Sun Jan 19 11:05:38 2014 +0100 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Sun Jan 19 22:38:17 2014 +0100 @@ -65,9 +65,9 @@ @{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false) *} -sledgehammer_params [provers = remote_z3, debug] +sledgehammer_params [provers = z3, debug] ML {* @{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true) *} -end \ No newline at end of file +end