diff --git a/Manual/Interaction/HOL-interaction.tex b/Manual/Interaction/HOL-interaction.tex
index dffcd30e94..a4b152f048 100644
--- a/Manual/Interaction/HOL-interaction.tex
+++ b/Manual/Interaction/HOL-interaction.tex
@@ -116,20 +116,20 @@
   stack} and then put together using the ML function {\tt prove}
 (Section~\ref{prove1}, \ref{prove2}). To start the goal stack:
 \begin{enum}
-\item Write a goal, \eg{} {\tt `!n{.}~n < n + 1`}, (we write $\forall$ as {\tt !} in HOL4).
+\item Write a goal, \eg{} {\tt `!n{.}~n~<~n~+~1`}, (we can write $\forall$ as {\tt !} in HOL4).
 \item Move the cursor inside the back-quotes ({\tt `}).
-\item Press {\tt M-h g} to push the goal onto the goal stack.
+\item Press {\tt M-h~g} to push the goal onto the goal stack.
 \end{enum}
 The HOL4 window should look something like this:
 \begin{code}
-- > val it =
-    Proof manager status: 1 proof.
-    1. Incomplete:
-         Initial goal:
-         !n. n < n + 1
+> val it =
+     Proof manager status: 1 proof.
+  1. Incomplete goalstack:
+       Initial goal:
+       \(\forall\)n. n < n + 1
 
-     : proofs
-- > val it = () : unit
+   : proofs
+> val it = () : unit
 \end{code}
 
 \mysubsec{Applying a tactic\label{apply}}
@@ -138,24 +138,24 @@
 
 \begin{enum}
 \item Write the name of a tactic, \eg{} {\tt decide\_tac},~see Section~\ref{tactics} for more tactics
-\item Press {\tt C-space} at one end of the text.
-\item Move the cursor to the other end of the text.
-\item Press {\tt M-h e} to apply the tactic.
+\item Select the text of the tactic
+\item Press {\tt M-h~e} to apply the tactic.
 \end{enum}
 A tactic makes HOL4 update the current goal. The HOL4 window will either
 display the new goal(s) or print:
 \begin{code}
     Initial goal proved.
-    |- !n. n < n + 1 : goalstack
+    |- \(\forall\)n. n < n + 1 : goalstack
 \end{code}
 You can undo the effect of the applied tactic by pressing {\tt M-h b}. Press {\tt M-h p} to view the current goal.
+To go all the way back to the start of the proof (to restart), press \texttt{M-h~R}.
 
 \mysubsec{Ending a goal-oriented proof}
 
 One can pop goals off the goal stack by pressing {\tt M-h d}, which gives:
 \begin{code}
-- - OK..
-> val it = There are currently no proofs. : proofs
+> OK..
+val it = There are currently no proofs. : proofs
 \end{code}
 
 \mysubsec{Saving the resulting theorem\label{prove1}}
@@ -166,10 +166,10 @@
 \begin{code}
 val LESS_ADD_1 = Q.prove({`} !n. n < n + 1 {`},decide_tac);
 \end{code}
-When the above line is copied into HOL4 (using {\tt C-space} then
+When the above line is copied into HOL4 (using text-selection then
 {\tt M-h M-r}, as described in Section~\ref{copy}), HOL4 responds with:
 \begin{code}
-- > val LESS_ADD_1 = |- !n. n < n + 1 : thm
+> val LESS_ADD_1 = |- !n. n < n + 1 : thm
 \end{code}
 
 \mysubsec{Saving proofs based on multiple tactics\label{prove2}}
@@ -192,8 +192,7 @@
   >- (asm_simp_tac bool_ss [MULT]
       >> decide_tac]));
 \end{code}
-Copy the above into HOL4 using {\tt C-space} then
-{\tt M-h M-r}, as in Section~\ref{copy}.
+Copy the above into HOL4 using text-selection, and then {\tt M-h M-r}, as in Section~\ref{copy}.
 
 \newcommand{\itemz}[2]{\texttt{#1}\; &-\;\; \textrm{#2}}
 \newcommand{\itemy}[2]{#1&\quad\quad&#2\\}
@@ -365,8 +364,8 @@
 
 Goals that contain top-level universal quantifiers ({\tt !x.}),
 implication ({\tt ==>}) or conjunction ({\tt \conj{}}) are often
-taken apart using {\tt\small REPEAT STRIP\_TAC} or just {\tt\small
-  STRIP\_TAC}, \eg{} the goal {\tt\small `!x{.}~(!z{.}~x < h z) ==> ?y{.}~f x = y`}
+taken apart using {\tt\small rpt strip\_tac} or just {\tt\small
+  strip\_tac}, \eg{} the goal {\tt\small `!x{.}~(!z{.}~x < h z) ==> ?y{.}~f x = y`}
 becomes the following. (Assumptions are written under the line.)
 \begin{code}
     ?y. f x = y
@@ -377,8 +376,8 @@
 \mysubsec{Existential quantifiers}
 
 Goals that have a top-level existential quantifier can be given a
-witness using {\tt \small Q.EXISTS\_TAC}, \eg{} {\tt \small
-  Q.EXISTS\_TAC `1`} applied to goal {\tt \small ?n{.}~!k{.}~n * k = k}
+witness using {\tt \small qexists\_tac}, \eg{} {\tt \small
+  qexists\_tac `1`} applied to goal {\tt \small ?n{.}~!k{.}~n * k = k}
 produces goal {\tt \small !k{.}~1 * k = k}.
 
 \mysubsec{Rewrites}
@@ -429,6 +428,7 @@
 Section~\ref{definition}.  One can start a complete (or strong)
 induction over the natural number {\tt\small n} using {\tt\small
   completeInduct\_on `n`}.
+As with \texttt{Cases\_on} one can also induct on terms (\eg, \texttt{\small Induct\_on~`hi~-~lo`}), though these proofs can be harder to carry out.
 
 \mysubsec{Case splits}
 
@@ -455,7 +455,8 @@
       0 < n
 \end{code}
 we might want to prove {\tt\small h n = g n} assuming {\tt\small 0 <
-  n}.  We can start such a subproof by typing {\tt\small `h n = g n`
+  n}.
+We can start such a subproof by typing {\tt\small `h n = g n`
   by ALL\_TAC}.\footnote{You can also use the emacs binding {\tt\small
     M-h M-s} with the cursor inside the sub-goal.} The new goal stack:
 \begin{code}