--- a/src/Doc/IsarRef/Document_Preparation.thy Wed Jan 22 22:32:28 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Wed Jan 22 23:19:10 2014 +0100
@@ -468,8 +468,11 @@
example.
The rail specification language is quoted here as Isabelle @{syntax
- string}; it has its own grammar given below.
+ string} or text @{syntax "cartouche"}; it has its own grammar given
+ below.
+ \begingroup
+ \def\isasymnewline{\isatext{\tt\isacharbackslash<newline>}}
@{rail \<open>
rule? + ';'
;
@@ -483,6 +486,7 @@
'@'? (string | @{syntax antiquotation}) |
'\<newline>'
\<close>}
+ \endgroup
The lexical syntax of @{text "identifier"} coincides with that of
@{syntax ident} in regular Isabelle syntax, but @{text string} uses