--- a/src/Doc/IsarRef/Outer_Syntax.thy Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy Sat Jan 18 19:15:12 2014 +0100
@@ -147,6 +147,7 @@
@{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree | "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
@{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
@{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
+ @{syntax_def cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
@{text letter} & = & @{text "latin | "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text " | "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text " | greek |"} \\
@@ -191,6 +192,11 @@
text is {\LaTeX} source, one may usually add some blank or comment
to avoid the critical character sequence.
+ A @{syntax_ref cartouche} consists of arbitrary text, with properly
+ balanced blocks of ``@{verbatim "\<open>"}~@{text "\<dots>"}~@{verbatim
+ "\<close>"}''. Note that the rendering of cartouche delimiters is
+ usually like this: ``@{text "\<open> \<dots> \<close>"}''.
+
Source comments take the form @{verbatim "(*"}~@{text
"\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
might prevent this. Note that this form indicates source comments