# HG changeset patch
# User nipkow
# Date 1675239266 -3600
# Node ID 9770db65d628fcd6620c309db9eb359bc5c528c5
# Parent  1310df9229bd8af77f0f7db30d2d5e7b19090d6b
tuning

diff -r 1310df9229bd -r 9770db65d628 src/Doc/Prog_Prove/Isar.thy
--- 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}}
diff -r 1310df9229bd -r 9770db65d628 src/Doc/Prog_Prove/Types_and_funs.thy
--- 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>