From 5d98d08ec227c302f528a44167c8abdeea6c2192 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Wed, 24 Jan 2024 10:39:05 +1100 Subject: [PATCH] [emacs-mode] Put DB "super match" into HOL/Misc menu --- tools/hol-mode.src | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tools/hol-mode.src b/tools/hol-mode.src index 80dc4191f2..66809a4e35 100644 --- a/tools/hol-mode.src +++ b/tools/hol-mode.src @@ -1925,6 +1925,9 @@ the surrounding text (as done by ‘hol-do-goal’ and (define-key global-map [menu-bar hol-menu hol-misc db-find] '("DB find" . hol-db-find)) +(define-key global-map [menu-bar hol-menu hol-misc db-match-with-selectors] + '("DB match (multiple selectors)" . hol-db-select)) + (define-key global-map [menu-bar hol-menu hol-misc db-match] '("DB match" . hol-db-match))