# HG changeset patch
# User wenzelm
# Date 1618952004 -7200
# Node ID e60333aa18cafe80545dc9b2c19ad746177c15b6
# Parent  c642c3cbbf0eefa3cf892e5ac2144120b86abbc4
proper use of antiquotations;

diff -r c642c3cbbf0e -r e60333aa18ca 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