diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 18:46:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 18:46:56 +0000 |
| commit | f025500ad0f5f7d7c21075ad5addc737e34bfd6f (patch) | |
| tree | a7e82a9604730b8697faef24c6c229a0cb18cd43 /hol-light | |
| parent | b0c6cae90829ba5b12a466716e4f3626e6cc70b5 (diff) | |
Add example menu entry
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) |