--- a/src/Doc/Prog_Prove/Isar.thy Tue Jan 31 19:07:24 2023 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy Wed Feb 01 09:14:26 2023 +0100
@@ -576,10 +576,10 @@
\begin{quote}
\isacom{have} \ \<open>"x > 0"\<close>\\
$\vdots$\\
-\isacom{from} \<open>`x>0`\<close> \dots\index{$IMP053@\<open>`...`\<close>}
+\isacom{from} \<open>\<open>x > 0\<close>\<close> \dots\index{$IMP053@\<open>`...`\<close>}
\end{quote}
-Note that the quotes around \<open>x>0\<close> are \conceptnoidx{back quotes}.
-They refer to the fact not by name but by value.
+The outside quotes in \<open>\<open>x > 0\<close>\<close> are the standard renderings of the symbols \texttt{\textbackslash<open>} and \texttt{\textbackslash<close>}.
+They refer to the fact not by name but ``by value''.
\subsection{\indexed{\isacom{moreover}}{moreover}}
\index{ultimately@\isacom{ultimately}}
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Tue Jan 31 19:07:24 2023 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Wed Feb 01 09:14:26 2023 +0100
@@ -324,7 +324,7 @@
(*>*)
apply(induction xs arbitrary: ys)
-txt\<open>The induction hypothesis is now universally quantified over \<open>ys\<close>:
+txt\<open>The induction hypothesis in the induction step is now universally quantified over \<open>ys\<close>:
@{subgoals[display,margin=65]}
Thus the proof succeeds:
\<close>