proper use of antiquotations;
authorwenzelm
Tue, 20 Apr 2021 22:53:24 +0200
changeset 73849 e60333aa18ca
parent 73848 c642c3cbbf0e
child 73850 5c4a09c4bc9c
child 73851 aece5cc9efb7
proper use of antiquotations;
src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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