aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-09-08 12:58:59 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-09-08 12:58:59 +0000
commitf445f4df6edd07068f91dbe04ea84059375781b7 (patch)
tree4ae62c2d8966ef5ec6e591d1218eb9451fb1080a /isar
parentfaa883a68c00a5a7275b2b42dbe97517e0d9fac2 (diff)
use-linear-undo: use default of t again
Diffstat (limited to 'isar')
-rw-r--r--isar/isar.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el
index 6a4e05a1..feea1f4d 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -257,7 +257,7 @@ See -k option for Isabelle interface script."
(setq proof-find-and-forget-fn 'isar-find-and-forget)
(setq proof-arbitrary-undo-positions nil)))
-(defpacustom use-linear-undo nil
+(defpacustom use-linear-undo t
"Whether to allow undo to re-enter completed proofs (requires restart)."
:type 'boolean
:eval (isar-set-undo-commands))