src/Doc/IsarRef/Inner_Syntax.thy

     @{syntax_def (inner) num_token} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
     @{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
   robust access to the respective tokens: the syntax tree holds a
   syntactic constant instead of a free variable.