[emacs-mode] Put DB "super match" into HOL/Misc menu

HOL-Theorem-Prover · Jan 23, 2024 · 5d98d08 · 5d98d08
1 parent ee5139a
commit 5d98d08
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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))