--- 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