aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-31 12:15:20 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-01-31 12:15:20 +0000
commitd52d7d723b6a48d77a8d399133f0633aed80777e (patch)
tree673900c12cffb29b54f9191ea0d09f224bc1380f /isar
parentf6e93d2ebdde09a3929e071bfe6a62992676f89c (diff)
auto-solve -> auto-solve-direct for Isabelle2011.
Diffstat (limited to 'isar')
-rw-r--r--isar/isar-autotest.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index 4207d28a..f24e3450 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -16,7 +16,7 @@
(proof-ready-for-assistant 'isar))
(declare-function isar-tracing:auto-quickcheck-toggle "isar.el")
-(declare-function isar-tracing:auto-solve-toggle "isar.el")
+(declare-function isar-tracing:auto-solve-direct-toggle "isar.el")
(declare-function isar-proof:parallel-proofs-toggle "isar.el")
(require 'pg-autotest)
@@ -49,7 +49,7 @@
;; Speed up prover
(pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
- (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
+ (pg-autotest eval (isar-tracing:auto-solve-direct-toggle 0)) ; autosolve hammers this!
(pg-autotest eval (proof-full-annotation-toggle 0))
(pg-autotest eval (isar-proof:parallel-proofs-toggle 0))
(proof-shell-wait)