doc/hol-mode/hol-mode.tex

9 \section*{Emacs HOL mode commands}
11 All of these commands are executed by first typing the HOL prefix
17 \item [h ``hol98''] Starts the HOL session.
18 \item [C-c ``hol-interrupt''] Interrupts the HOL session.  Useful for
20 \item [C-l ``hol-recentre''] Recentres the screen that HOL is running
23 \item [C-v ``hol-scroll-up''] Scrolls the HOL window.
32 \item [M-r   ``send-region''] Sends the \emph{region} to the HOL
35 \item [M-v ``hol-scroll-down''] Scrolls the HOL window.
39 \item [e ``expand-hol-tactic''] Sends the region to the HOL process as
42   (delimited on both sides by back-quotes) to the HOL process.  With a
45 \item [l ``hol-load-file''] Loads a HOL library.  If there is a region