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}}