diff -r b49366215417 -r 8e8243975860 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Fri Jan 17 20:51:36 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Sat Jan 18 19:15:12 2014 +0100
@@ -633,14 +633,16 @@
     @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
 
     @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
+    @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
 
   The token categories @{syntax (inner) num_token}, @{syntax (inner)
-  float_token}, @{syntax (inner) xnum_token}, and @{syntax (inner)
-  str_token} are not used in Pure.  Object-logics may implement numerals
-  and string constants by adding appropriate syntax declarations,
-  together with some translation functions (e.g.\ see Isabelle/HOL).
+  float_token}, @{syntax (inner) xnum_token}, @{syntax (inner)
+  str_token}, and @{syntax (inner) cartouche} are not used in Pure.
+  Object-logics may implement numerals and string literals by adding
+  appropriate syntax declarations, together with some translation
+  functions (e.g.\ see Isabelle/HOL).
 
   The derived categories @{syntax_def (inner) num_const}, @{syntax_def
   (inner) float_const}, and @{syntax_def (inner) num_const} provide