diff -r df68d656d5c4 -r 15261d78d7b5 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Thu Feb 06 22:10:16 2025 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Fri Feb 07 21:27:11 2025 +0100
@@ -486,8 +486,7 @@
 \<close>
 lemma True
 proof -
-  \<comment> \<open>pretty trivial\<close>
-  show True by force
+  show True by (rule TrueI)
 qed
 text_raw \<open>
   \end{minipage}\end{center}
@@ -498,21 +497,20 @@
 
 \begin{quote}
 \small
-\verb!text_raw {!\verb!*!\\
+\verb!text_raw \!\verb!<open>!\\
 \verb!  \begin{figure}!\\
 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
 \verb!  \isastyleminor\isamarkuptrue!\\
-\verb!*!\verb!}!\\
+\verb!\!\verb!<close>!\\
 \verb!lemma True!\\
 \verb!proof -!\\
-\verb!  -- "pretty trivial"!\\
-\verb!  show True by force!\\
+\verb!  show True by (rule TrueI)!\\
 \verb!qed!\\
-\verb!text_raw {!\verb!*!\\
+\verb!text_raw \!\verb!<open>!\\
 \verb!  \end{minipage}\end{center}!\\
 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
 \verb!  \end{figure}!\\
-\verb!*!\verb!}!
+\verb!\!\verb!<close>!
 \end{quote}
 
 Other theory text, e.g.\ definitions, can be put in figures, too.