# HG changeset patch
# User nipkow
# Date 1675239280 -3600
# Node ID 646e36bf24aeca5658b82dea3f38215b35f7648b
# Parent  7ceed24c88dc8529f37abe81e9691e5014e4462f# Parent  9770db65d628fcd6620c309db9eb359bc5c528c5
merged

diff -r 7ceed24c88dc -r 646e36bf24ae src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Tue Jan 31 23:17:44 2023 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy	Wed Feb 01 09:14:40 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}}
diff -r 7ceed24c88dc -r 646e36bf24ae src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Tue Jan 31 23:17:44 2023 +0100
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Wed Feb 01 09:14:40 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>