aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2013-01-15 14:40:18 +0000
committerGravatar Hendrik Tews <hendrik@askra.de>2013-01-15 14:40:18 +0000
commite1c67a6cb5ba78af5faf43b87c1869de5f3161b9 (patch)
treefda7893a1f89c9da4564598312664059473b75b8 /hol-light
parente8afd3f63521dcf847b8b47fdffbcf65859acbde (diff)
- support bullets and braces in Prooftree
- prooftree protocol change to version 3
Diffstat (limited to 'hol-light')
-rw-r--r--hol-light/hol-light.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index f3c983b0..3201e2ff 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -400,7 +400,7 @@ the currently open proof.")
proof-tree-find-begin-of-unfinished-proof
'hol-light-find-begin-of-unfinished-proof
;; These ones belong in shell mode
- proof-tree-proof-finished-regexp "No subgoals"
+ proof-tree-branch-finished-regexp "No subgoals"
proof-tree-show-sequent-command
(lambda (id) (format "print_xgoal_of_id \"%s\";;" id))