src/Doc/IsarRef/Generic.thy

 
   \begin{matharray}{rcll}
     @{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}
   
   \item @{command "print_options"} prints the available configuration
   options, with names, types, and current values.

     @{method_def elim} & : & @{text method} \\
     @{method_def succeed} & : & @{text method} \\
     @{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}
   
   \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text
   "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout

     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
     @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{attribute tagged} @{syntax name} @{syntax name}
     ;
     @@{attribute untagged} @{syntax name}
     ;
     @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref}
     ;
     (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs}
     ;
     @@{attribute rotated} @{syntax int}?
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{attribute tagged}~@{text "name value"} and @{attribute
   untagged}~@{text name} add and remove \emph{tags} of some theorem.

     @{method_def subst} & : & @{text method} \\
     @{method_def hypsubst} & : & @{text method} \\
     @{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,
   single step calculations would be performed in a structured text
   (see also \secref{sec:calculation}), while the Simplifier methods

     @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
     @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
     @{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} )
     ;
     @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)

     ;
     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
     ;
 
     dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
-  "}
+  \<close>}
 
 \begin{description}
 
   \item @{method rule_tac} etc. do resolution of rules with explicit
   instantiation.  This works the same way as the ML tactics @{ML

   \begin{matharray}{rcl}
     @{method_def simp} & : & @{text method} \\
     @{method_def simp_all} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
     ;
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
     @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{method simp} invokes the Simplifier on the first subgoal,
   after inserting chained facts as additional goal premises; further

     @{attribute_def split} & : & @{text attribute} \\
     @{attribute_def cong} & : & @{text attribute} \\
     @{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}
 
   \item @{attribute simp} declares rewrite rules, by adding or
   deleting them from the simpset within the theory or proof context.

   \begin{matharray}{rcl}
     @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     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}
 
   \item @{command "simproc_setup"} defines a named simplification
   procedure that is invoked by the Simplifier whenever any of the

 text {*
   \begin{matharray}{rcl}
     @{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}
   
   \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to
   be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>,

     @{attribute_def rule} & : & @{text attribute} \\
     @{attribute_def iff} & : & @{text attribute} \\
     @{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}
 
   \item @{command "print_claset"} prints the collection of rules
   declared to the Classical Reasoner, i.e.\ the @{ML_type claset}

   \begin{matharray}{rcl}
     @{method_def rule} & : & @{text method} \\
     @{method_def contradiction} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method rule} @{syntax thmrefs}?
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{method rule} as offered by the Classical Reasoner is a
   refinement over the Pure one (see \secref{sec:pure-meth-att}).  Both

     @{method_def slowsimp} & : & @{text method} \\
     @{method_def bestsimp} & : & @{text method} \\
     @{method_def deepen} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{method blast} @{syntax nat}? (@{syntax clamod} * )
     ;
     @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * )
     ;
     @@{method force} (@{syntax clasimpmod} * )

     ;
     @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') |
       ('cong' | 'split') (() | 'add' | 'del') |
       'iff' (((() | 'add') '?'?) | 'del') |
       (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs}
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{method blast} is a separate classical tableau prover that
   uses the same classical rule declarations as explained before.

     @{method_def safe} & : & @{text method} \\
     @{method_def clarify} & : & @{text method} \\
     @{method_def clarsimp} & : & @{text method} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{method safe} | @@{method clarify}) (@{syntax clamod} * )
     ;
     @@{method clarsimp} (@{syntax clasimpmod} * )
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{method safe} repeatedly performs safe steps on all subgoals.
   It is deterministic, with at most one outcome.

   Isabelle/FOL or Isabelle/HOL may be taken as realistic examples.
 
   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}
   
   \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant
   @{text c} as the truth judgment of the current object-logic.  Its