From f025500ad0f5f7d7c21075ad5addc737e34bfd6f Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Wed, 8 Feb 2012 18:46:56 +0000
Subject: Add example menu entry

---
 hol-light/hol-light.el | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'hol-light')

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)
-- 
cgit v1.2.3