--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Apr 19 21:57:52 2021 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Tue Apr 20 22:53:24 2021 +0200
@@ -146,7 +146,7 @@
is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches do not have this limitation.
A @{syntax_ref cartouche} consists of arbitrary text, with properly balanced
- blocks of ``\<^verbatim>\<open>\<open>\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>\<close>\<close>''. Note that the rendering
+ blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested: the text is