diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 18:51:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 18:51:29 +0000 |
| commit | 8c8086c8c50a4f68aa429091f7d3b3e31e97bb34 (patch) | |
| tree | c588035495eae003020101267117100c2d6f120c /isar/isar-autotest.el | |
| parent | 99861ac0e7596d85834d34b95ac770e2b4c7e296 (diff) | |
Fix compilation
Diffstat (limited to 'isar/isar-autotest.el')
| -rw-r--r-- | isar/isar-autotest.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index d86dcdf6..123c519c 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -8,6 +8,9 @@ (eval-when-compile (require 'cl)) +(declare-function isar-tracing:auto-quickcheck-toggle "isar.el") +(declare-function isar-tracing:auto-solve-toggle "isar.el") + (require 'proof-utils) (require 'pg-autotest) @@ -25,7 +28,7 @@ (pg-autotest remark "Testing random jumps") (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) - (pg-autotest eval (isar-tracing:auto-solve 0)) ; autosolve hammers this! + (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! (pg-autotest script-randomjumps "isar/Example.thy" 5) (pg-autotest script-randomjumps "etc/isar/AHundredTheorems.thy" 10) |