# HG changeset patch
# User wenzelm
# Date 1390406525 -3600
# Node ID b1a5d603fd121e20a37e1d778f0ff09de98b51ff
# Parent  5792f5106c4042cfe67fab9239fc7a586c715e13
prefer rail cartouche -- avoid back-slashed quotes;
proper documentation of \<newline> syntax;

diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -457,12 +457,12 @@
   @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command datatype_new} target? @{syntax dt_options}? \<newline>
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
   @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code' | 'rep_compat') + ',') ')'
-"}
+\<close>}
 
 The syntactic entity \synt{target} can be used to specify a local
 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
@@ -491,13 +491,13 @@
 The left-hand sides of the datatype equations specify the name of the type to
 define, its type parameters, and additional information:
 
-@{rail "
+@{rail \<open>
   @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
   ;
   @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
-"}
+\<close>}
 
 \noindent
 The syntactic entity \synt{name} denotes an identifier, \synt{typefree}
@@ -510,10 +510,10 @@
 Inside a mutually recursive specification, all defined datatypes must
 mention exactly the same type variables in the same order.
 
-@{rail "
+@{rail \<open>
   @{syntax_def ctor}: (name ':')? name (@{syntax ctor_arg} * ) \<newline>
     @{syntax dt_sel_defaults}? mixfix?
-"}
+\<close>}
 
 \medskip
 
@@ -523,9 +523,9 @@
 can be supplied at the front to override the default name
 (@{text t.is_C\<^sub>j}).
 
-@{rail "
+@{rail \<open>
   @{syntax_def ctor_arg}: type | '(' name ':' type ')'
-"}
+\<close>}
 
 \medskip
 
@@ -535,9 +535,9 @@
 (@{text un_C\<^sub>ji}). The same selector names can be reused for several
 constructors as long as they share the same type.
 
-@{rail "
+@{rail \<open>
   @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
-"}
+\<close>}
 
 \noindent
 Given a constructor
@@ -558,9 +558,9 @@
   @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command datatype_new_compat} names
-"}
+\<close>}
 
 \noindent
 The old datatype package provides some functionality that is not yet replicated
@@ -1352,11 +1352,11 @@
   @{command_def "primrec_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command primrec_new} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
   ;
   @{syntax_def pr_equation}: thmdecl? prop
-"}
+\<close>}
 *}
 
 
@@ -1574,10 +1574,10 @@
   @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command codatatype} target? \<newline>
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
-"}
+\<close>}
 
 \noindent
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
@@ -2241,7 +2241,7 @@
   @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
     @{syntax pcr_option}? fixes @'where'
     (@{syntax pcr_formula} + '|')
@@ -2249,7 +2249,7 @@
   @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
   ;
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
-"}
+\<close>}
 
 The optional target is potentially followed by a corecursion-specific option:
 
@@ -2325,11 +2325,11 @@
   @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command bnf} target? (name ':')? typ \<newline>
     'map:' term ('sets:' (term +))? 'bd:' term \<newline>
     ('wits:' (term +))? ('rel:' term)?
-"}
+\<close>}
 *}
 
 
@@ -2342,7 +2342,7 @@
   @{text "bnf_decl"} & : & @{text "local_theory \<rightarrow> local_theory"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command bnf_decl} target? @{syntax dt_name}
   ;
   @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
@@ -2350,7 +2350,7 @@
   @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
-"}
+\<close>}
 
 Declares a fresh type and fresh constants (map, set, relator, cardinal bound)
 and asserts the bnf properties for these constants as axioms. Additionally,
@@ -2370,9 +2370,9 @@
   @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command print_bnfs}
-"}
+\<close>}
 *}
 
 
@@ -2416,7 +2416,7 @@
   @{command_def "wrap_free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
 \end{matharray}
 
-@{rail "
+@{rail \<open>
   @@{command wrap_free_constructors} target? @{syntax dt_options} \<newline>
     term_list name @{syntax wfc_discs_sels}?
   ;
@@ -2425,7 +2425,7 @@
   @{syntax_def name_term}: (name ':' term)
   ;
   X_list: '[' (X + ',') ']'
-"}
+\<close>}
 
 % options: no_discs_sels no_code rep_compat
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarImplementation/Isar.thy
--- a/src/Doc/IsarImplementation/Isar.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarImplementation/Isar.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -563,9 +563,9 @@
   @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation attributes} attributes
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -196,7 +196,7 @@
   @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation class} nameref
   ;
   @@{ML_antiquotation sort} sort
@@ -206,7 +206,7 @@
    @@{ML_antiquotation nonterminal}) nameref
   ;
   @@{ML_antiquotation typ} type
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -444,7 +444,7 @@
   @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   (@@{ML_antiquotation const_name} |
    @@{ML_antiquotation const_abbrev}) nameref
   ;
@@ -453,7 +453,7 @@
   @@{ML_antiquotation term} term
   ;
   @@{ML_antiquotation prop} prop
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -780,7 +780,7 @@
   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation ctyp} typ
   ;
   @@{ML_antiquotation cterm} term
@@ -793,7 +793,7 @@
   ;
   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \<newline>
     @'by' method method?
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -666,9 +666,9 @@
   concept of \emph{ML antiquotation}.  The standard token language of
   ML is augmented by special syntactic entities of the following form:
 
-  @{rail "
+  @{rail \<open>
   @{syntax_def antiquote}: '@{' nameref args '}'
-  "}
+  \<close>}
 
   Here @{syntax nameref} and @{syntax args} are regular outer syntax
   categories \cite{isabelle-isar-ref}.  Attributes and proof methods
@@ -699,9 +699,9 @@
   @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation make_string}
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarImplementation/Prelim.thy
--- a/src/Doc/IsarImplementation/Prelim.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -165,11 +165,11 @@
   @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation theory} nameref?
   ;
   @@{ML_antiquotation theory_context} nameref
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1025,9 +1025,9 @@
   @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
   @@{ML_antiquotation binding} name
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Document_Preparation.thy
--- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -47,13 +47,13 @@
   markup commands, but have a different status within Isabelle/Isar
   syntax.
 
-  @{rail "
+  @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
       @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
     ;
     (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} |
       @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -148,7 +148,7 @@
   context.
 
   %% FIXME less monolithic presentation, move to individual sections!?
-  @{rail "
+  @{rail \<open>
     '@{' antiquotation '}'
     ;
     @{syntax_def antiquotation}:
@@ -176,7 +176,7 @@
       @@{antiquotation ML_op} options @{syntax name} |
       @@{antiquotation ML_type} options @{syntax name} |
       @@{antiquotation ML_struct} options @{syntax name} |
-      @@{antiquotation \"file\"} options @{syntax name} |
+      @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name}
     ;
@@ -187,7 +187,7 @@
     styles: '(' (style + ',') ')'
     ;
     style: (@{syntax name} +)
-  "}
+  \<close>}
 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
@@ -404,11 +404,11 @@
   presentation tags, to indicate some modification in the way it is
   printed in the document.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def tags}: ( tag * )
     ;
     tag: '%' (@{syntax ident} | @{syntax string})
-  "}
+  \<close>}
 
   Some tags are pre-declared for certain classes of commands, serving
   as default markup if no tags are given in the text:
@@ -457,7 +457,7 @@
     @{antiquotation_def "rail"} & : & @{text antiquotation} \\
   \end{matharray}
 
-  @{rail "'rail' string"}
+  @{rail \<open>'rail' (string | cartouche)\<close>}
 
   The @{antiquotation rail} antiquotation allows to include syntax
   diagrams into Isabelle documents.  {\LaTeX} requires the style file
@@ -468,7 +468,7 @@
   The rail specification language is quoted here as Isabelle @{syntax
   string}; it has its own grammar given below.
 
-  @{rail "
+  @{rail \<open>
   rule? + ';'
   ;
   rule: ((identifier | @{syntax antiquotation}) ':')? body
@@ -479,8 +479,8 @@
   ;
   atom: '(' body? ')' | identifier |
     '@'? (string | @{syntax antiquotation}) |
-    '\\\\\\\\'
-  "}
+    '\<newline>'
+  \<close>}
 
   The lexical syntax of @{text "identifier"} coincides with that of
   @{syntax ident} in regular Isabelle syntax, but @{text string} uses
@@ -496,62 +496,62 @@
 
   \item Empty @{verbatim "()"}
 
-  @{rail "()"}
+  @{rail \<open>()\<close>}
 
   \item Nonterminal @{verbatim "A"}
 
-  @{rail "A"}
+  @{rail \<open>A\<close>}
 
   \item Nonterminal via Isabelle antiquotation
   @{verbatim "@{syntax method}"}
 
-  @{rail "@{syntax method}"}
+  @{rail \<open>@{syntax method}\<close>}
 
   \item Terminal @{verbatim "'xyz'"}
 
-  @{rail "'xyz'"}
+  @{rail \<open>'xyz'\<close>}
 
   \item Terminal in keyword style @{verbatim "@'xyz'"}
 
-  @{rail "@'xyz'"}
+  @{rail \<open>@'xyz'\<close>}
 
   \item Terminal via Isabelle antiquotation
   @{verbatim "@@{method rule}"}
 
-  @{rail "@@{method rule}"}
+  @{rail \<open>@@{method rule}\<close>}
 
   \item Concatenation @{verbatim "A B C"}
 
-  @{rail "A B C"}
+  @{rail \<open>A B C\<close>}
 
   \item Newline inside concatenation
   @{verbatim "A B C \<newline> D E F"}
 
-  @{rail "A B C \<newline> D E F"}
+  @{rail \<open>A B C \<newline> D E F\<close>}
 
   \item Variants @{verbatim "A | B | C"}
 
-  @{rail "A | B | C"}
+  @{rail \<open>A | B | C\<close>}
 
   \item Option @{verbatim "A ?"}
 
-  @{rail "A ?"}
+  @{rail \<open>A ?\<close>}
 
   \item Repetition @{verbatim "A *"}
 
-  @{rail "A *"}
+  @{rail \<open>A *\<close>}
 
   \item Repetition with separator @{verbatim "A * sep"}
 
-  @{rail "A * sep"}
+  @{rail \<open>A * sep\<close>}
 
   \item Strict repetition @{verbatim "A +"}
 
-  @{rail "A +"}
+  @{rail \<open>A +\<close>}
 
   \item Strict repetition with separator @{verbatim "A + sep"}
 
-  @{rail "A + sep"}
+  @{rail \<open>A + sep\<close>}
 
   \end{itemize}
 *}
@@ -564,10 +564,9 @@
     @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command display_drafts} (@{syntax name} +)
-
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -34,9 +34,9 @@
     @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -70,14 +70,14 @@
     @{method_def fail} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
     ;
     (@@{method erule} | @@{method drule} | @@{method frule})
       ('(' @{syntax nat} ')')? @{syntax thmrefs}
     ;
     (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -136,7 +136,7 @@
     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute tagged} @{syntax name} @{syntax name}
     ;
     @@{attribute untagged} @{syntax name}
@@ -146,7 +146,7 @@
     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
     ;
     @@{attribute rotated} @{syntax int}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -201,11 +201,11 @@
     @{method_def split} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method subst} ('(' 'asm' ')')? \<newline> ('(' (@{syntax nat}+) ')')? @{syntax thmref}
     ;
     @@{method split} @{syntax thmrefs}
-  "}
+  \<close>}
 
   These methods provide low-level facilities for equational reasoning
   that are intended for specialized applications only.  Normally,
@@ -304,7 +304,7 @@
     @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
       @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
@@ -319,7 +319,7 @@
     ;
 
     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
-  "}
+  \<close>}
 
 \begin{description}
 
@@ -406,7 +406,7 @@
     @{method_def simp_all} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
     ;
 
@@ -414,7 +414,7 @@
     ;
     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -608,10 +608,10 @@
     @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
       (() | 'add' | 'del')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -923,13 +923,13 @@
     simproc & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
       @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
     ;
 
     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1229,12 +1229,12 @@
     @{attribute_def simplified} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute simplified} opt? @{syntax thmrefs}?
     ;
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -1490,13 +1490,13 @@
     @{attribute_def swapped} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}?
     ;
     @@{attribute rule} 'del'
     ;
     @@{attribute iff} (((() | 'add') '?'?) | 'del')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1562,9 +1562,9 @@
     @{method_def contradiction} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method rule} @{syntax thmrefs}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1603,7 +1603,7 @@
     @{method_def deepen} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
     ;
     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
@@ -1624,7 +1624,7 @@
       ('cong' | 'split') (() | 'add' | 'del') |
       'iff' (((() | 'add') '?'?) | 'del') |
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1735,11 +1735,11 @@
     @{method_def clarsimp} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
     ;
     @@{method clarsimp} (@{syntax clasimpmod} * )
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1926,13 +1926,13 @@
   Generic tools may refer to the information provided by object-logic
   declarations internally.
 
-  @{rail "
+  @{rail \<open>
     @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
     ;
     @@{attribute atomize} ('(' 'full' ')')?
     ;
     @@{attribute rule_format} ('(' 'noasm' ')')?
-  "}
+  \<close>}
 
   \begin{description}
   
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -96,17 +96,17 @@
   introduction rule.  The default rule declarations of Isabelle/HOL
   already take care of most common situations.
 
-  @{rail "
+  @{rail \<open>
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
     @{syntax target}? \<newline>
-    @{syntax \"fixes\"} (@'for' @{syntax \"fixes\"})? (@'where' clauses)? \<newline>
+    @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
     (@'monos' @{syntax thmrefs})?
     ;
     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
     @@{attribute (HOL) mono} (() | 'add' | 'del')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -264,11 +264,11 @@
     @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
-  @{rail "
-    @@{command (HOL) primrec} @{syntax target}? @{syntax \"fixes\"} @'where' equations
+  @{rail \<open>
+    @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
     ;
     (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
-      @{syntax \"fixes\"} \<newline> @'where' equations
+      @{syntax "fixes"} \<newline> @'where' equations
     ;
 
     equations: (@{syntax thmdecl}? @{syntax prop} + '|')
@@ -278,7 +278,7 @@
     @@{command (HOL) termination} @{syntax term}?
     ;
     @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -508,7 +508,7 @@
     @{method_def (HOL) induction_schema} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method (HOL) relation} @{syntax term}
     ;
     @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
@@ -518,7 +518,7 @@
     @@{method (HOL) induction_schema}
     ;
     orders: ( 'max' | 'min' | 'ms' ) *
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -574,11 +574,11 @@
     @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) partial_function} @{syntax target}?
-      '(' @{syntax nameref} ')' @{syntax \"fixes\"} \<newline>
+      '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
       @'where' @{syntax thmdecl}? @{syntax prop}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -649,7 +649,7 @@
   "recdef_tc"} for defining recursive are mostly obsolete; @{command
   (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
       @{syntax name} @{syntax term} (@{syntax prop} +) hints?
     ;
@@ -661,7 +661,7 @@
       (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
     ;
     tc: @{syntax nameref} ('(' @{syntax nat} ')')?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -695,10 +695,10 @@
     @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
       @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
-  "}
+  \<close>}
 *}
 
 
@@ -710,7 +710,7 @@
     @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) datatype} (spec + @'and')
     ;
     @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
@@ -719,7 +719,7 @@
     spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
     ;
     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -873,12 +873,12 @@
     @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
       (@{syntax type} '+')? (constdecl +)
     ;
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1074,14 +1074,13 @@
   type_synonym} from Isabelle/Pure merely introduces syntactic
   abbreviations, without any logical significance.
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) typedef} abs_type '=' rep_set
     ;
-
     abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
     ;
     rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1198,10 +1197,9 @@
     @{command_def (HOL) "enriched_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) enriched_type} (@{syntax name} ':')? @{syntax term}
-    ;
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1265,28 +1263,26 @@
   packages. The user should consider using these two new packages for
   lifting definitions and transporting theorems.
 
-  @{rail "
-    @@{command (HOL) quotient_type} (spec);
-
+  @{rail \<open>
+    @@{command (HOL) quotient_type} (spec)
+    ;
     spec: @{syntax typespec} @{syntax mixfix}? '=' \<newline>
      @{syntax type} '/' ('partial' ':')? @{syntax term} \<newline>
-     (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?;
-  "}
-
-  @{rail "
+     (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?
+  \<close>}
+
+  @{rail \<open>
     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
-    @{syntax term} 'is' @{syntax term};
-
+    @{syntax term} 'is' @{syntax term}
+    ;
     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
-  "}
-
-  @{rail "
+  \<close>}
+
+  @{rail \<open>
     @@{method (HOL) lifting} @{syntax thmrefs}?
     ;
-
     @@{method (HOL) lifting_setup} @{syntax thmrefs}?
-    ;
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1399,12 +1395,12 @@
     @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   \end{matharray}
 
-  @{rail "
-  (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
-    '(' (decl +) ')' \<newline> (@{syntax thmdecl}? @{syntax prop} +)
-  ;
-  decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
-  "}
+  @{rail \<open>
+    (@@{command (HOL) specification} | @@{command (HOL) ax_specification})
+      '(' (decl +) ')' \<newline> (@{syntax thmdecl}? @{syntax prop} +)
+    ;
+    decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?)
+  \<close>}
 
   \begin{description}
 
@@ -1458,10 +1454,10 @@
   @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
   @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
 
-  @{rail "
+  @{rail \<open>
     (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
-    (@{syntax nameref} (@{syntax term} + ) + @'and')
-  "}
+      (@{syntax nameref} (@{syntax term} + ) + @'and')
+  \<close>}
 
   \begin{description}
 
@@ -1490,9 +1486,9 @@
     @{attribute_def (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute (HOL) split_format} ('(' 'complete' ')')?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1626,27 +1622,27 @@
     @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\   
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \<newline>
       @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
-  "}
-
-  @{rail "
+  \<close>}
+
+  @{rail \<open>
     @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
       'is' @{syntax term} (@'parametric' @{syntax thmref})?;
-  "}
-
-  @{rail "
+  \<close>}
+
+  @{rail \<open>
     @@{command (HOL) lifting_forget} @{syntax nameref};
-  "}
-
-  @{rail "
+  \<close>}
+
+  @{rail \<open>
     @@{command (HOL) lifting_update} @{syntax nameref};
-  "}
-
-  @{rail "
+  \<close>}
+
+  @{rail \<open>
     @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1828,14 +1824,11 @@
   them as necessary when parsing a term. See
   \cite{traytel-berghofer-nipkow-2011} for details.
 
-  @{rail "
+  @{rail \<open>
     @@{attribute (HOL) coercion} (@{syntax term})?
     ;
-  "}
-  @{rail "
     @@{attribute (HOL) coercion_map} (@{syntax term})?
-    ;
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1902,9 +1895,9 @@
     @{method_def (HOL) iprover} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
-    @@{method (HOL) iprover} ( @{syntax rulemod} * )
-  "}
+  @{rail \<open>
+    @@{method (HOL) iprover} (@{syntax rulemod} *)
+  \<close>}
 
   \begin{description}
 
@@ -1934,14 +1927,13 @@
     @{method_def (HOL) "metis"} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method (HOL) meson} @{syntax thmrefs}?
     ;
-
     @@{method (HOL) metis}
       ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
       @{syntax thmrefs}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1968,13 +1960,13 @@
     @{attribute_def (HOL) algebra} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method (HOL) algebra}
       ('add' ':' @{syntax thmrefs})?
       ('del' ':' @{syntax thmrefs})?
     ;
     @@{attribute (HOL) algebra} (() | 'add' | 'del')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -2051,9 +2043,9 @@
     @{method_def (HOL) "coherent"} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method (HOL) coherent} @{syntax thmrefs}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -2081,7 +2073,7 @@
     @{command_def (HOL) "sledgehammer_params"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) try}
     ;
 
@@ -2094,13 +2086,10 @@
 
     @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
     ;
-
     args: ( @{syntax name} '=' value + ',' )
     ;
-
     facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thmrefs} ) + ) ? ')'
-    ;
-  "} % FIXME check args "value"
+  \<close>} % FIXME check args "value"
 
   \begin{description}
 
@@ -2150,7 +2139,7 @@
     @{command_def (HOL) "find_unused_assms"} & : & @{text "context \<rightarrow>"}
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
     ;
 
@@ -2171,13 +2160,10 @@
 
     @@{command (HOL) find_unused_assms} @{syntax name}?
     ;
-
     modes: '(' (@{syntax name} +) ')'
     ;
-
     args: ( @{syntax name} '=' value + ',' )
-    ;
-  "} % FIXME check "value"
+  \<close>} % FIXME check "value"
 
   \begin{description}
 
@@ -2320,7 +2306,7 @@
     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
     ;
     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
@@ -2329,9 +2315,8 @@
     ;
     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
     ;
-
     rule: 'rule' ':' @{syntax thmref}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -2413,7 +2398,7 @@
     @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (HOL) export_code} ( constexpr + ) \<newline>
        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
         ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
@@ -2553,7 +2538,7 @@
     ;
 
     modes: mode @'as' const
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -46,7 +46,7 @@
   These diagnostic commands assist interactive development by printing
   internal logical entities in a human-readable fashion.
 
-  @{rail "
+  @{rail \<open>
     @@{command typ} @{syntax modes}? @{syntax type} ('::' @{syntax sort})?
     ;
     @@{command term} @{syntax modes}? @{syntax term}
@@ -59,9 +59,8 @@
     ;
     @@{command print_state} @{syntax modes}?
     ;
-
     @{syntax_def modes}: '(' (@{syntax name} + ) ')'
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -358,7 +357,7 @@
   to specify any context-free priority grammar, which is more general
   than the fixity declarations of ML and Prolog.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def mixfix}: '('
       @{syntax template} prios? @{syntax nat}? |
       (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
@@ -369,7 +368,7 @@
     template: string
     ;
     prios: '[' (@{syntax nat} + ',') ']'
-  "}
+  \<close>}
 
   The string given as @{text template} may include literal text,
   spacing, blocks, and arguments (denoted by ``@{text _}''); the
@@ -559,7 +558,7 @@
   allows to add or delete mixfix annotations for of existing logical
   entities within the current context.
 
-  @{rail "
+  @{rail \<open>
     (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
       @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
@@ -567,7 +566,7 @@
       (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
     @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1217,7 +1216,7 @@
   @{command translations}) are required to turn resulting parse trees
   into proper representations of formal entities again.
 
-  @{rail "
+  @{rail \<open>
     @@{command nonterminal} (@{syntax name} + @'and')
     ;
     (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
@@ -1231,7 +1230,7 @@
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
     transpat: ('(' @{syntax nameref} ')')? @{syntax string}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1464,7 +1463,7 @@
   manipulations of inner syntax, at the expense of some complexity and
   obscurity in the implementation.
 
-  @{rail "
+  @{rail \<open>
   ( @@{command parse_ast_translation} | @@{command parse_translation} |
     @@{command print_translation} | @@{command typed_print_translation} |
     @@{command print_ast_translation}) @{syntax text}
@@ -1473,7 +1472,7 @@
    @@{ML_antiquotation type_syntax} |
    @@{ML_antiquotation const_syntax} |
    @@{ML_antiquotation syntax_const}) name
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Misc.thy
--- a/src/Doc/IsarRef/Misc.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Misc.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -20,7 +20,7 @@
     @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command print_theory} | @@{command print_theorems}) ('!'?)
     ;
 
@@ -37,7 +37,7 @@
     @@{command thm_deps} @{syntax thmrefs}
     ;
     @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
-  "}
+  \<close>}
 
   These commands print certain parts of the theory and proof context.
   Note that there are some further ones available, such as for the set
@@ -121,9 +121,9 @@
     @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command cd} | @@{command use_thy}) @{syntax name}
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Outer_Syntax.thy
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -72,9 +72,9 @@
     @{command_def "help"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command help} (@{syntax name} * )
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -233,14 +233,14 @@
   Already existing objects are usually referenced by @{syntax
   nameref}.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def name}: @{syntax ident} | @{syntax symident} |
       @{syntax string} | @{syntax nat}
     ;
     @{syntax_def parname}: '(' @{syntax name} ')'
     ;
     @{syntax_def nameref}: @{syntax name} | @{syntax longident}
-  "}
+  \<close>}
 *}
 
 
@@ -250,11 +250,11 @@
   natural numbers and floating point numbers.  These are combined as
   @{syntax int} and @{syntax real} as follows.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
     ;
     @{syntax_def real}: @{syntax float} | @{syntax int}
-  "}
+  \<close>}
 
   Note that there is an overlap with the category @{syntax name},
   which also includes @{syntax nat}.
@@ -271,11 +271,11 @@
   @{verbatim "--"}~@{syntax text}.  Any number of these may occur
   within Isabelle/Isar commands.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def text}: @{syntax verbatim} | @{syntax nameref}
     ;
     @{syntax_def comment}: '--' @{syntax text}
-  "}
+  \<close>}
 *}
 
 
@@ -288,13 +288,13 @@
   intersection of these classes.  The syntax of type arities is given
   directly at the outer level.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
     ;
     @{syntax_def sort}: @{syntax nameref}
     ;
     @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
-  "}
+  \<close>}
 *}
 
 
@@ -314,38 +314,38 @@
   by commands or other keywords already (such as @{verbatim "="} or
   @{verbatim "+"}).
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
       @{syntax typevar}
     ;
     @{syntax_def term}: @{syntax nameref} | @{syntax var}
     ;
     @{syntax_def prop}: @{syntax term}
-  "}
+  \<close>}
 
   Positional instantiations are indicated by giving a sequence of
   terms, or the placeholder ``@{text _}'' (underscore), which means to
   skip a position.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def inst}: '_' | @{syntax term}
     ;
     @{syntax_def insts}: (@{syntax inst} *)
-  "}
+  \<close>}
 
   Type declarations and definitions usually refer to @{syntax
   typespec} on the left-hand side.  This models basic type constructor
   application at the outer syntax level.  Note that only plain postfix
   notation is available here, but no infixes.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def typespec}:
       (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
     ;
     @{syntax_def typespec_sorts}:
       (() | (@{syntax typefree} ('::' @{syntax sort})?) |
         '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
-  "}
+  \<close>}
 *}
 
 
@@ -356,11 +356,11 @@
   specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}''.
   This works both for @{syntax term} and @{syntax prop}.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
     ;
     @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
-  "}
+  \<close>}
 
   \medskip Declarations of local variables @{text "x :: \<tau>"} and
   logical propositions @{text "a : \<phi>"} represent different views on
@@ -370,11 +370,11 @@
   references of current facts).  In any case, Isar proof elements
   usually admit to introduce multiple such items simultaneously.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
     ;
     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
-  "}
+  \<close>}
 
   The treatment of multiple declarations corresponds to the
   complementary focus of @{syntax vars} versus @{syntax props}.  In
@@ -398,7 +398,7 @@
   any atomic entity, including any @{syntax keyword} conforming to
   @{syntax symident}.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
       @{syntax keyword} | @{syntax cartouche}
@@ -408,7 +408,7 @@
     @{syntax_def args}: arg *
     ;
     @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
-  "}
+  \<close>}
 
   Theorem specifications come in several flavors: @{syntax axmdecl}
   and @{syntax thmdecl} usually refer to axioms, assumptions or
@@ -443,7 +443,7 @@
   This form of in-place declarations is particularly useful with
   commands like @{command "declare"} and @{command "using"}.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
     ;
     @{syntax_def thmdecl}: thmbind ':'
@@ -460,7 +460,7 @@
     thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
     ;
     selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
-  "}
+  \<close>}
 *}
 
 end
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -53,11 +53,11 @@
     @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command notepad} @'begin'
     ;
     @@{command end}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -183,7 +183,7 @@
   exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
   \<phi>[t]"}.
 
-  @{rail "
+  @{rail \<open>
     @@{command fix} (@{syntax vars} + @'and')
     ;
     (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
@@ -192,7 +192,7 @@
     ;
     def: @{syntax thmdecl}? \<newline>
       @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -262,9 +262,9 @@
   input process just after type checking.  Also note that @{command
   "def"} does not support polymorphism.
 
-  @{rail "
+  @{rail \<open>
     @@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and')
-  "}
+  \<close>}
 
   The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
   @{syntax prop_pat} (see \secref{sec:term-decls}).
@@ -318,12 +318,12 @@
   to the most recently established facts, but only \emph{before}
   issuing a follow-up claim.
 
-  @{rail "
+  @{rail \<open>
     @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
     ;
     (@@{command from} | @@{command with} | @@{command using} | @@{command unfolding})
       (@{syntax thmrefs} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -429,7 +429,7 @@
   contexts of (essentially a big disjunction of eliminated parameters
   and assumptions, cf.\ \secref{sec:obtain}).
 
-  @{rail "
+  @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
      @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
@@ -441,12 +441,12 @@
   
     goal: (@{syntax props} + @'and')
     ;
-    longgoal: @{syntax thmdecl}? (@{syntax_ref \"includes\"}?) (@{syntax context_elem} * ) conclusion
+    longgoal: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} * ) conclusion
     ;
     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
     ;
     case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -541,12 +541,12 @@
   nameref}~@{syntax args} specifications.  Note that parentheses may
   be dropped for single method specifications (with no arguments).
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def method}:
       (@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']')
     ;
     methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | '|')
-  "}
+  \<close>}
 
   Proper Isar proof methods do \emph{not} admit arbitrary goal
   addressing, but refer either to the first sub-goal or all sub-goals
@@ -564,10 +564,10 @@
   all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
   "n"}.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def goal_spec}:
       '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
-  "}
+  \<close>}
 *}
 
 
@@ -621,15 +621,15 @@
   default terminal method.  Any remaining goals are always solved by
   assumption in the very last step.
 
-  @{rail "
+  @{rail \<open>
     @@{command proof} method?
     ;
     @@{command qed} method?
     ;
-    @@{command \"by\"} method method?
+    @@{command "by"} method method?
     ;
-    (@@{command \".\"} | @@{command \"..\"} | @@{command sorry})
-  "}
+    (@@{command "."} | @@{command ".."} | @@{command sorry})
+  \<close>}
 
   \begin{description}
   
@@ -706,7 +706,7 @@
     @{attribute_def "where"} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method fact} @{syntax thmrefs}?
     ;
     @@{method (Pure) rule} @{syntax thmrefs}?
@@ -723,10 +723,10 @@
     ;
     @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
     ;
-    @@{attribute \"where\"}
+    @@{attribute "where"}
       ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
       (@{syntax type} | @{syntax term}) * @'and')
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -846,13 +846,13 @@
     @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     ( @@{command apply} | @@{command apply_end} ) @{syntax method}
     ;
     @@{command defer} @{syntax nat}?
     ;
     @@{command prefer} @{syntax nat}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -907,10 +907,9 @@
     @{command_def "method_setup"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
-    ;
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -963,12 +962,12 @@
   later, provided that the corresponding parameters do \emph{not}
   occur in the conclusion.
 
-  @{rail "
+  @{rail \<open>
     @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')
       @'where' (@{syntax props} + @'and')
     ;
     @@{command guess} (@{syntax vars} + @'and')
-  "}
+  \<close>}
 
   The derived Isar command @{command "obtain"} is defined as follows
   (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
@@ -1078,11 +1077,11 @@
     @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')?
     ;
     @@{attribute trans} (() | 'add' | 'del')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1195,7 +1194,7 @@
   derived manually become ready to use in advanced case analysis
   later.
 
-  @{rail "
+  @{rail \<open>
     @@{command case} (caseref | '(' caseref (('_' | @{syntax name}) *) ')')
     ;
     caseref: nameref attributes?
@@ -1208,7 +1207,7 @@
     @@{attribute params} ((@{syntax name} * ) + @'and')
     ;
     @@{attribute consumes} @{syntax int}?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -1303,7 +1302,7 @@
   the names of the facts in the local context invoked by the @{command "case"}
   command.
 
-  @{rail "
+  @{rail \<open>
     @@{method cases} ('(' 'no_simp' ')')? \<newline>
       (@{syntax insts} * @'and') rule?
     ;
@@ -1322,7 +1321,7 @@
     arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +)
     ;
     taking: 'taking' ':' @{syntax insts}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1499,7 +1498,7 @@
     @{attribute_def coinduct} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute cases} spec
     ;
     @@{attribute induct} spec
@@ -1508,7 +1507,7 @@
     ;
 
     spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
-  "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -50,7 +50,7 @@
   although some user-interfaces might pretend that trailing input is
   admissible.
 
-  @{rail "
+  @{rail \<open>
     @@{command theory} @{syntax name} imports keywords? \<newline> @'begin'
     ;
     imports: @'imports' (@{syntax name} +)
@@ -59,7 +59,7 @@
     ;
     keyword_decls: (@{syntax string} +)
       ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -121,13 +121,13 @@
   targets, like @{command "locale"}, @{command "class"}, @{command
   "instantiation"}, @{command "overloading"}.
 
-  @{rail "
+  @{rail \<open>
     @@{command context} @{syntax nameref} @'begin'
     ;
-    @@{command context} @{syntax_ref \"includes\"}? (@{syntax context_elem} * ) @'begin'
+    @@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin'
     ;
     @{syntax_def target}: '(' @'in' @{syntax nameref} ')'
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -210,14 +210,14 @@
   without logical dependencies, which is in contrast to locales and
   locale interpretation (\secref{sec:locale}).
 
-  @{rail "
+  @{rail \<open>
     @@{command bundle} @{syntax target}? \<newline>
     @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
     ;
     (@@{command include} | @@{command including}) (@{syntax nameref}+)
     ;
-    @{syntax_def \"includes\"}: @'includes' (@{syntax nameref}+)
-  "}
+    @{syntax_def "includes"}: @'includes' (@{syntax nameref}+)
+  \<close>}
 
   \begin{description}
 
@@ -274,8 +274,8 @@
   "defs"} (see \secref{sec:consts}), and raw axioms.  In particular,
   type-inference covers the whole specification as usual.
 
-  @{rail "
-    @@{command axiomatization} @{syntax \"fixes\"}? (@'where' specs)?
+  @{rail \<open>
+    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
     ;
     @@{command definition} @{syntax target}? \<newline>
       (decl @'where')? @{syntax thmdecl}? @{syntax prop}
@@ -284,13 +284,13 @@
       (decl @'where')? @{syntax prop}
     ;
 
-    @{syntax_def \"fixes\"}: ((@{syntax name} ('::' @{syntax type})?
+    @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
       @{syntax mixfix}? | @{syntax vars}) + @'and')
     ;
     specs: (@{syntax thmdecl}? @{syntax props} + @'and')
     ;
     decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -364,12 +364,12 @@
   case: it consists of a theorem which is applied to the context by
   means of an attribute.
 
-  @{rail "
+  @{rail \<open>
     (@@{command declaration} | @@{command syntax_declaration})
       ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
     ;
     @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -431,8 +431,8 @@
   elements from the locale instances.  Redundant locale instances are
   omitted according to roundup.
 
-  @{rail "
-    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
+  @{rail \<open>
+    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))?
     ;
     instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
     ;
@@ -441,7 +441,7 @@
     pos_insts: ('_' | @{syntax term})*
     ;
     named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
-  "}
+  \<close>}
 
   A locale instance consists of a reference to a locale and either
   positional or named parameter instantiations.  Identical
@@ -483,7 +483,7 @@
 
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
-  @{rail "
+  @{rail \<open>
     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
     ;
     @@{command print_locale} '!'? @{syntax nameref}
@@ -492,12 +492,12 @@
       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
     ;
     @{syntax_def context_elem}:
-      @'fixes' (@{syntax \"fixes\"} + @'and') |
+      @'fixes' (@{syntax "fixes"} + @'and') |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
       @'notes' (@{syntax thmdef}? @{syntax thmrefs} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -630,7 +630,7 @@
   "interpretation"}) and also within proof bodies (@{command
   "interpret"}).
 
-  @{rail "
+  @{rail \<open>
     @@{command interpretation} @{syntax locale_expr} equations?
     ;
     @@{command interpret} @{syntax locale_expr} equations?
@@ -644,7 +644,7 @@
     ;
 
     equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and')
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -796,7 +796,7 @@
   (notably type-inference).  See \cite{isabelle-classes} for a short
   tutorial.
 
-  @{rail "
+  @{rail \<open>
     @@{command class} class_spec @'begin'?
     ;
     class_spec: @{syntax name} '='
@@ -809,7 +809,7 @@
       @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
     ;
     @@{command subclass} @{syntax target}? @{syntax nameref}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -968,11 +968,11 @@
   The @{command "overloading"} target provides a convenient view for
   end-users.
 
-  @{rail "
+  @{rail \<open>
     @@{command overloading} ( spec + ) @'begin'
     ;
     spec: @{syntax name} ( '==' | '\<equiv>' ) @{syntax term} ( '(' @'unchecked' ')' )?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1010,14 +1010,14 @@
     @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command ML_file} @{syntax name}
     ;
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     ;
     @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1094,13 +1094,13 @@
     @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command classes} (@{syntax classdecl} +)
     ;
     @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
     ;
     @@{command default_sort} @{syntax sort}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1141,13 +1141,13 @@
     @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
     ;
     @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
     ;
     @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1219,13 +1219,13 @@
   corresponding occurrences on some right-hand side need to be an
   instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
 
-  @{rail "
+  @{rail \<open>
     @@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +)
     ;
     @@{command defs} opt? (@{syntax axmdecl} @{syntax prop} +)
     ;
     opt: '(' @'unchecked'? @'overloaded'? ')'
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1259,11 +1259,11 @@
     @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
       (@{syntax thmdef}? @{syntax thmrefs} + @'and')
       (@'for' (@{syntax vars} + @'and'))?
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -1302,9 +1302,9 @@
   asserted, and records within the internal derivation object how
   presumed theorems depend on unproven suppositions.
 
-  @{rail "
+  @{rail \<open>
     @@{command oracle} @{syntax name} '=' @{syntax text}
-  "}
+  \<close>}
 
   \begin{description}
 
@@ -1333,10 +1333,10 @@
     @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     ( @{command hide_class} | @{command hide_type} |
       @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax nameref} + )
-  "}
+  \<close>}
 
   Isabelle organizes any kind of name declarations (of types,
   constants, theorems etc.) by separate hierarchically structured name
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -48,7 +48,7 @@
   mode @{verbatim "isabelle-root"} for session ROOT files, which is
   enabled by default for any file of that name.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def session_chapter}: @'chapter' @{syntax name}
     ;
 
@@ -73,7 +73,7 @@
     theories: @'theories' opts? ( @{syntax name} * )
     ;
     files: @'files' ( @{syntax name} + )
-    "}
+  \<close>}
 
   \begin{description}
 
diff -r 5792f5106c40 -r b1a5d603fd12 src/Doc/ZF/ZF_Isar.thy
--- a/src/Doc/ZF/ZF_Isar.thy	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Doc/ZF/ZF_Isar.thy	Wed Jan 22 17:02:05 2014 +0100
@@ -24,9 +24,9 @@
     @{attribute_def (ZF) TC} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute (ZF) TC} (() | 'add' | 'del')
-  "}
+  \<close>}
 
   \begin{description}
   
@@ -59,7 +59,7 @@
     @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
     ;
 
@@ -67,22 +67,22 @@
     ;
     intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
     ;
-    hints: @{syntax (ZF) \"monos\"}? condefs? \<newline>
+    hints: @{syntax (ZF) "monos"}? condefs? \<newline>
       @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
     ;
-    @{syntax_def (ZF) \"monos\"}: @'monos' @{syntax thmrefs}
+    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
     ;
     condefs: @'con_defs' @{syntax thmrefs}
     ;
     @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
     ;
     @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
-  "}
+  \<close>}
 
   In the following syntax specification @{text "monos"}, @{text
   typeintros}, and @{text typeelims} are the same as above.
 
-  @{rail "
+  @{rail \<open>
     (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
     ;
 
@@ -92,8 +92,8 @@
     ;
     con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
     ;
-    hints: @{syntax (ZF) \"monos\"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
-  "}
+    hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
+  \<close>}
 
   See \cite{isabelle-ZF} for further information on inductive
   definitions in ZF, but note that this covers the old-style theory
@@ -108,9 +108,9 @@
     @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
-  "}
+  \<close>}
 *}
 
 
@@ -127,14 +127,13 @@
     @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
     ;
     @@{method (ZF) ind_cases} (@{syntax prop} +)
     ;
     @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
-    ;
-  "}
+  \<close>}
 *}
 
 end
diff -r 5792f5106c40 -r b1a5d603fd12 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Wed Jan 22 16:03:11 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Wed Jan 22 17:02:05 2014 +0100
@@ -266,7 +266,7 @@
 
 val _ = Theory.setup
   (Thy_Output.antiquotation @{binding rail}
-    (Scan.lift (Parse.source_position Parse.string))
+    (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
     (fn {state, ...} => output_rules state o read));
 
 end;