From e01e18bc7d940efee4acb82b1aef27e082686831 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 8 Feb 2018 11:08:40 +1100 Subject: [PATCH] Mention M-h m as keybinding for print_match in interaction guide --- Manual/Interaction/HOL-interaction.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/Manual/Interaction/HOL-interaction.tex b/Manual/Interaction/HOL-interaction.tex index 21fb7a9a3c..04e645845a 100644 --- a/Manual/Interaction/HOL-interaction.tex +++ b/Manual/Interaction/HOL-interaction.tex @@ -337,6 +337,7 @@ {\tt\small print\_match [] \sq \sq n DIV m\sq\sq} returns a list of length 32. Note that {\tt\small print\_match [] \sq \sq DIV\sq\sq} does not work since {\tt\small DIV} is an infix operator, but {\tt\small print\_match [] \sq \sq \$DIV\sq \sq} works. +The key-binding \texttt{M-h~m} (and the menu entry ``DB match'') will prompt for the term pattern to search for, and pass this query onto the HOL session (saving the need to type \texttt{print\_match~[]} and the enclosing quotation marks). \mysec{Common proof tactics\label{tactics}}