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