# HG changeset patch
# User wenzelm
# Date 1390407249 -3600
# Node ID 497693486858c936145a1a95322aa1e5e26bc765
# Parent  b1a5d603fd121e20a37e1d778f0ff09de98b51ff
tuned;

diff -r b1a5d603fd12 -r 497693486858 src/Doc/IsarRef/Document_Preparation.thy
--- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 17:02:05 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 17:14:09 2014 +0100
@@ -457,7 +457,9 @@
     @{antiquotation_def "rail"} & : & @{text antiquotation} \\
   \end{matharray}
 
-  @{rail \<open>'rail' (string | cartouche)\<close>}
+  @{rail \<open>
+    'rail' (@{syntax string} | @{syntax cartouche})
+  \<close>}
 
   The @{antiquotation rail} antiquotation allows to include syntax
   diagrams into Isabelle documents.  {\LaTeX} requires the style file
@@ -485,7 +487,7 @@
   The lexical syntax of @{text "identifier"} coincides with that of
   @{syntax ident} in regular Isabelle syntax, but @{text string} uses
   single quotes instead of double quotes of the standard @{syntax
-  string} category, to avoid extra escapes.
+  string} category.
 
   Each @{text rule} defines a formal language (with optional name),
   using a notation that is similar to EBNF or regular expressions with