diff options
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/hol-light.el | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index a0afba1a..f3c983b0 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -500,4 +500,13 @@ The not yet delayed output is in the region (add-hook 'proof-tree-urgent-action-hook 'hol-light-proof-tree-get-new-subgoals) +;;; +;;; Menu commands +;;; + +(proof-definvisible hol-light-dump-proof "dump_proof();;") + +(defpgdefault menu-entries + '(["Dump refactored proof" hol-light-dump-proof t])) + (provide 'hol-light) |