--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:34:28 2015 +0200
@@ -135,7 +135,7 @@
argument that is a cartouche.
Omitting the control symbol is also possible: a cartouche without special
- decoration is equivalent to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
+ decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
special name @{antiquotation_def cartouche} is defined in the context:
Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}