diff -r 3480725c71d2 -r 0debd22f0c0e src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Tue Oct 20 23:53:40 2015 +0200
@@ -5,40 +5,36 @@
 chapter \<open>Tactical reasoning\<close>
 
 text \<open>Tactical reasoning works by refining an initial claim in a
-  backwards fashion, until a solved form is reached.  A @{text "goal"}
+  backwards fashion, until a solved form is reached.  A \<open>goal\<close>
   consists of several subgoals that need to be solved in order to
   achieve the main statement; zero subgoals means that the proof may
-  be finished.  A @{text "tactic"} is a refinement operation that maps
-  a goal to a lazy sequence of potential successors.  A @{text
-  "tactical"} is a combinator for composing tactics.\<close>
+  be finished.  A \<open>tactic\<close> is a refinement operation that maps
+  a goal to a lazy sequence of potential successors.  A \<open>tactical\<close> is a combinator for composing tactics.\<close>
 
 
 section \<open>Goals \label{sec:tactical-goals}\<close>
 
 text \<open>
   Isabelle/Pure represents a goal as a theorem stating that the
-  subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
-  C"}.  The outermost goal structure is that of a Horn Clause: i.e.\
+  subgoals imply the main goal: \<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
+  C\<close>.  The outermost goal structure is that of a Horn Clause: i.e.\
   an iterated implication without any quantifiers\footnote{Recall that
-  outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
-  variables in the body: @{text "\<phi>[?x]"}.  These variables may get
-  instantiated during the course of reasoning.}.  For @{text "n = 0"}
+  outermost \<open>\<And>x. \<phi>[x]\<close> is always represented via schematic
+  variables in the body: \<open>\<phi>[?x]\<close>.  These variables may get
+  instantiated during the course of reasoning.}.  For \<open>n = 0\<close>
   a goal is called ``solved''.
 
-  The structure of each subgoal @{text "A\<^sub>i"} is that of a
-  general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
-  \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}.  Here @{text
-  "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
-  arbitrary-but-fixed entities of certain types, and @{text
-  "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
+  The structure of each subgoal \<open>A\<^sub>i\<close> is that of a
+  general Hereditary Harrop Formula \<open>\<And>x\<^sub>1 \<dots>
+  \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B\<close>.  Here \<open>x\<^sub>1, \<dots>, x\<^sub>k\<close> are goal parameters, i.e.\
+  arbitrary-but-fixed entities of certain types, and \<open>H\<^sub>1, \<dots>, H\<^sub>m\<close> are goal hypotheses, i.e.\ facts that may
   be assumed locally.  Together, this forms the goal context of the
-  conclusion @{text B} to be established.  The goal hypotheses may be
+  conclusion \<open>B\<close> to be established.  The goal hypotheses may be
   again arbitrary Hereditary Harrop Formulas, although the level of
   nesting rarely exceeds 1--2 in practice.
 
-  The main conclusion @{text C} is internally marked as a protected
-  proposition, which is represented explicitly by the notation @{text
-  "#C"} here.  This ensures that the decomposition into subgoals and
+  The main conclusion \<open>C\<close> is internally marked as a protected
+  proposition, which is represented explicitly by the notation \<open>#C\<close> here.  This ensures that the decomposition into subgoals and
   main conclusion is well-defined for arbitrarily structured claims.
 
   \<^medskip>
@@ -46,8 +42,8 @@
   Isabelle/Pure rules:
 
   \[
-  \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
-  \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
+  \infer[\<open>(init)\<close>]{\<open>C \<Longrightarrow> #C\<close>}{} \qquad
+  \infer[\<open>(finish)\<close>]{\<open>C\<close>}{\<open>#C\<close>}
   \]
 
   \<^medskip>
@@ -55,10 +51,10 @@
   with protected propositions:
 
   \[
-  \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
+  \infer[\<open>(protect n)\<close>]{\<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C\<close>}{\<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C\<close>}
   \]
   \[
-  \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
+  \infer[\<open>(conclude)\<close>]{\<open>A \<Longrightarrow> \<dots> \<Longrightarrow> C\<close>}{\<open>A \<Longrightarrow> \<dots> \<Longrightarrow> #C\<close>}
   \]
 \<close>
 
@@ -70,26 +66,26 @@
   @{index_ML Goal.conclude: "thm -> thm"} \\
   \end{mldecls}
 
-  \<^descr> @{ML "Goal.init"}~@{text C} initializes a tactical goal from
-  the well-formed proposition @{text C}.
+  \<^descr> @{ML "Goal.init"}~\<open>C\<close> initializes a tactical goal from
+  the well-formed proposition \<open>C\<close>.
 
-  \<^descr> @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
-  @{text "thm"} is a solved goal (no subgoals), and concludes the
+  \<^descr> @{ML "Goal.finish"}~\<open>ctxt thm\<close> checks whether theorem
+  \<open>thm\<close> is a solved goal (no subgoals), and concludes the
   result by removing the goal protection.  The context is only
   required for printing error messages.
 
-  \<^descr> @{ML "Goal.protect"}~@{text "n thm"} protects the statement
-  of theorem @{text "thm"}.  The parameter @{text n} indicates the
+  \<^descr> @{ML "Goal.protect"}~\<open>n thm\<close> protects the statement
+  of theorem \<open>thm\<close>.  The parameter \<open>n\<close> indicates the
   number of premises to be retained.
 
-  \<^descr> @{ML "Goal.conclude"}~@{text "thm"} removes the goal
+  \<^descr> @{ML "Goal.conclude"}~\<open>thm\<close> removes the goal
   protection, even if there are pending subgoals.
 \<close>
 
 
 section \<open>Tactics\label{sec:tactics}\<close>
 
-text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
+text \<open>A \<open>tactic\<close> is a function \<open>goal \<rightarrow> goal\<^sup>*\<^sup>*\<close> that
   maps a given goal state (represented as a theorem, cf.\
   \secref{sec:tactical-goals}) to a lazy sequence of potential
   successor states.  The underlying sequence implementation is lazy
@@ -121,7 +117,7 @@
   schematic goal variables).
 
   Tactics with explicit \<^emph>\<open>subgoal addressing\<close> are of the form
-  @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
+  \<open>int \<rightarrow> tactic\<close> and may be applied to a particular subgoal
   (counting from 1).  If the subgoal number is out of range, the
   tactic should fail with an empty result sequence, but must not raise
   an exception!
@@ -139,7 +135,7 @@
   very common error when implementing tactics!
 
   Tactics with internal subgoal addressing should expose the subgoal
-  index as @{text "int"} argument in full generality; a hardwired
+  index as \<open>int\<close> argument in full generality; a hardwired
   subgoal 1 is not acceptable.
   
   \<^medskip>
@@ -195,16 +191,16 @@
   \<^descr> @{ML all_tac} is a tactic that always succeeds, returning a
   singleton sequence with unchanged goal state.
 
-  \<^descr> @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
+  \<^descr> @{ML print_tac}~\<open>ctxt message\<close> is like @{ML all_tac}, but
   prints a message together with the goal state on the tracing
   channel.
 
-  \<^descr> @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
+  \<^descr> @{ML PRIMITIVE}~\<open>rule\<close> turns a primitive inference rule
   into a tactic with unique result.  Exception @{ML THM} is considered
   a regular tactic failure and produces an empty result; other
   exceptions are passed through.
 
-  \<^descr> @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
+  \<^descr> @{ML SUBGOAL}~\<open>(fn (subgoal, i) => tactic)\<close> is the
   most basic form to produce a tactic with subgoal addressing.  The
   given abstraction over the subgoal term and subgoal number allows to
   peek at the relevant information of the full goal state.  The
@@ -215,14 +211,14 @@
   avoids expensive re-certification in situations where the subgoal is
   used directly for primitive inferences.
 
-  \<^descr> @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
-  specified subgoal @{text "i"}.  This rearranges subgoals and the
+  \<^descr> @{ML SELECT_GOAL}~\<open>tac i\<close> confines a tactic to the
+  specified subgoal \<open>i\<close>.  This rearranges subgoals and the
   main goal protection (\secref{sec:tactical-goals}), while retaining
   the syntactic context of the overall goal state (concerning
   schematic variables etc.).
 
-  \<^descr> @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
-  @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but
+  \<^descr> @{ML PREFER_GOAL}~\<open>tac i\<close> rearranges subgoals to put
+  \<open>i\<close> in front.  This is similar to @{ML SELECT_GOAL}, but
   without changing the main goal protection.
 \<close>
 
@@ -237,7 +233,7 @@
   \<^emph>\<open>Destruct-resolution\<close> is like elim-resolution, but the given
   destruction rules are first turned into canonical elimination
   format.  \<^emph>\<open>Forward-resolution\<close> is like destruct-resolution, but
-  without deleting the selected assumption.  The @{text "r/e/d/f"}
+  without deleting the selected assumption.  The \<open>r/e/d/f\<close>
   naming convention is maintained for several different kinds of
   resolution rules and tactics.
 
@@ -281,20 +277,19 @@
   @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state
+  \<^descr> @{ML resolve_tac}~\<open>ctxt thms i\<close> refines the goal state
   using the given theorems, which should normally be introduction
-  rules.  The tactic resolves a rule's conclusion with subgoal @{text
-  i}, replacing it by the corresponding versions of the rule's
+  rules.  The tactic resolves a rule's conclusion with subgoal \<open>i\<close>, replacing it by the corresponding versions of the rule's
   premises.
 
-  \<^descr> @{ML eresolve_tac}~@{text "ctxt thms i"} performs elim-resolution
+  \<^descr> @{ML eresolve_tac}~\<open>ctxt thms i\<close> performs elim-resolution
   with the given theorems, which are normally be elimination rules.
 
   Note that @{ML_text "eresolve_tac ctxt [asm_rl]"} is equivalent to @{ML_text
   "assume_tac ctxt"}, which facilitates mixing of assumption steps with
   genuine eliminations.
 
-  \<^descr> @{ML dresolve_tac}~@{text "ctxt thms i"} performs
+  \<^descr> @{ML dresolve_tac}~\<open>ctxt thms i\<close> performs
   destruct-resolution with the given theorems, which should normally
   be destruction rules.  This replaces an assumption by the result of
   applying one of the rules.
@@ -303,21 +298,20 @@
   selected assumption is not deleted.  It applies a rule to an
   assumption, adding the result as a new assumption.
 
-  \<^descr> @{ML biresolve_tac}~@{text "ctxt brls i"} refines the proof state
+  \<^descr> @{ML biresolve_tac}~\<open>ctxt brls i\<close> refines the proof state
   by resolution or elim-resolution on each rule, as indicated by its
-  flag.  It affects subgoal @{text "i"} of the proof state.
+  flag.  It affects subgoal \<open>i\<close> of the proof state.
 
-  For each pair @{text "(flag, rule)"}, it applies resolution if the
-  flag is @{text "false"} and elim-resolution if the flag is @{text
-  "true"}.  A single tactic call handles a mixture of introduction and
+  For each pair \<open>(flag, rule)\<close>, it applies resolution if the
+  flag is \<open>false\<close> and elim-resolution if the flag is \<open>true\<close>.  A single tactic call handles a mixture of introduction and
   elimination rules, which is useful to organize the search process
   systematically in proof tools.
 
-  \<^descr> @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i}
+  \<^descr> @{ML assume_tac}~\<open>ctxt i\<close> attempts to solve subgoal \<open>i\<close>
   by assumption (modulo higher-order unification).
 
   \<^descr> @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
-  only for immediate @{text "\<alpha>"}-convertibility instead of using
+  only for immediate \<open>\<alpha>\<close>-convertibility instead of using
   unification.  It succeeds (with a unique next state) if one of the
   assumptions is equal to the subgoal's conclusion.  Since it does not
   instantiate variables, it cannot make other subgoals unprovable.
@@ -346,25 +340,22 @@
   higher-order unification is not so useful.  This typically involves
   rules like universal elimination, existential introduction, or
   equational substitution.  Here the unification problem involves
-  fully flexible @{text "?P ?x"} schemes, which are hard to manage
+  fully flexible \<open>?P ?x\<close> schemes, which are hard to manage
   without further hints.
 
-  By providing a (small) rigid term for @{text "?x"} explicitly, the
-  remaining unification problem is to assign a (large) term to @{text
-  "?P"}, according to the shape of the given subgoal.  This is
+  By providing a (small) rigid term for \<open>?x\<close> explicitly, the
+  remaining unification problem is to assign a (large) term to \<open>?P\<close>, according to the shape of the given subgoal.  This is
   sufficiently well-behaved in most practical situations.
 
   \<^medskip>
-  Isabelle provides separate versions of the standard @{text
-  "r/e/d/f"} resolution tactics that allow to provide explicit
+  Isabelle provides separate versions of the standard \<open>r/e/d/f\<close> resolution tactics that allow to provide explicit
   instantiations of unknowns of the given rule, wrt.\ terms that refer
   to the implicit context of the selected subgoal.
 
-  An instantiation consists of a list of pairs of the form @{text
-  "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
-  the given rule, and @{text t} is a term from the current proof
+  An instantiation consists of a list of pairs of the form \<open>(?x, t)\<close>, where \<open>?x\<close> is a schematic variable occurring in
+  the given rule, and \<open>t\<close> is a term from the current proof
   context, augmented by the local goal parameters of the selected
-  subgoal; cf.\ the @{text "focus"} operation described in
+  subgoal; cf.\ the \<open>focus\<close> operation described in
   \secref{sec:variables}.
 
   Entering the syntactic context of a subgoal is a brittle operation,
@@ -373,8 +364,7 @@
   global names.  Explicit renaming of subgoal parameters prior to
   explicit instantiation might help to achieve a bit more robustness.
 
-  Type instantiations may be given as well, via pairs like @{text
-  "(?'a, \<tau>)"}.  Type instantiations are distinguished from term
+  Type instantiations may be given as well, via pairs like \<open>(?'a, \<tau>)\<close>.  Type instantiations are distinguished from term
   instantiations by the syntactic form of the schematic variable.
   Types are instantiated before terms are.  Since term instantiation
   already performs simple type-inference, so explicit type
@@ -402,9 +392,9 @@
   @{index_ML rename_tac: "string list -> int -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
-  rule @{text thm} with the instantiations @{text insts}, as described
-  above, and then performs resolution on subgoal @{text i}.
+  \<^descr> @{ML Rule_Insts.res_inst_tac}~\<open>ctxt insts thm i\<close> instantiates the
+  rule \<open>thm\<close> with the instantiations \<open>insts\<close>, as described
+  above, and then performs resolution on subgoal \<open>i\<close>.
   
   \<^descr> @{ML Rule_Insts.eres_inst_tac} is like @{ML Rule_Insts.res_inst_tac},
   but performs elim-resolution.
@@ -415,20 +405,19 @@
   \<^descr> @{ML Rule_Insts.forw_inst_tac} is like @{ML Rule_Insts.dres_inst_tac}
   except that the selected assumption is not deleted.
 
-  \<^descr> @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
-  @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
-  same as a new subgoal @{text "i + 1"} (in the original context).
+  \<^descr> @{ML Rule_Insts.subgoal_tac}~\<open>ctxt \<phi> i\<close> adds the proposition
+  \<open>\<phi>\<close> as local premise to subgoal \<open>i\<close>, and poses the
+  same as a new subgoal \<open>i + 1\<close> (in the original context).
 
-  \<^descr> @{ML Rule_Insts.thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
-  premise from subgoal @{text i}.  Note that @{text \<phi>} may contain
+  \<^descr> @{ML Rule_Insts.thin_tac}~\<open>ctxt \<phi> i\<close> deletes the specified
+  premise from subgoal \<open>i\<close>.  Note that \<open>\<phi>\<close> may contain
   schematic variables, to abbreviate the intended proposition; the
   first matching subgoal premise will be deleted.  Removing useless
   premises from a subgoal increases its readability and can make
   search tactics run faster.
 
-  \<^descr> @{ML rename_tac}~@{text "names i"} renames the innermost
-  parameters of subgoal @{text i} according to the provided @{text
-  names} (which need to be distinct identifiers).
+  \<^descr> @{ML rename_tac}~\<open>names i\<close> renames the innermost
+  parameters of subgoal \<open>i\<close> according to the provided \<open>names\<close> (which need to be distinct identifiers).
 
 
   For historical reasons, the above instantiation tactics take
@@ -453,9 +442,9 @@
   @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal
-  @{text i} by @{text n} positions: from right to left if @{text n} is
-  positive, and from left to right if @{text n} is negative.
+  \<^descr> @{ML rotate_tac}~\<open>n i\<close> rotates the premises of subgoal
+  \<open>i\<close> by \<open>n\<close> positions: from right to left if \<open>n\<close> is
+  positive, and from left to right if \<open>n\<close> is negative.
 
   \<^descr> @{ML distinct_subgoals_tac} removes duplicate subgoals from a
   proof state.  This is potentially inefficient.
@@ -489,24 +478,21 @@
   @{index_ML_op COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
-  \<^descr> @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
-  @{text "i"} using @{text "rule"}, without lifting.  The @{text
-  "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
-  @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
-  number of new subgoals.  If @{text "flag"} is @{text "true"} then it
-  performs elim-resolution --- it solves the first premise of @{text
-  "rule"} by assumption and deletes that assumption.
+  \<^descr> @{ML compose_tac}~\<open>ctxt (flag, rule, m) i\<close> refines subgoal
+  \<open>i\<close> using \<open>rule\<close>, without lifting.  The \<open>rule\<close> is taken to have the form \<open>\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>\<close>, where
+  \<open>\<psi>\<close> need not be atomic; thus \<open>m\<close> determines the
+  number of new subgoals.  If \<open>flag\<close> is \<open>true\<close> then it
+  performs elim-resolution --- it solves the first premise of \<open>rule\<close> by assumption and deletes that assumption.
 
-  \<^descr> @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
-  regarded as an atomic formula, to solve premise @{text "i"} of
-  @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
-  "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that
-  unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
-  \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as
+  \<^descr> @{ML Drule.compose}~\<open>(thm\<^sub>1, i, thm\<^sub>2)\<close> uses \<open>thm\<^sub>1\<close>,
+  regarded as an atomic formula, to solve premise \<open>i\<close> of
+  \<open>thm\<^sub>2\<close>.  Let \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> be \<open>\<psi>\<close> and \<open>\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>\<close>.  The unique \<open>s\<close> that
+  unifies \<open>\<psi>\<close> and \<open>\<phi>\<^sub>i\<close> yields the theorem \<open>(\<phi>\<^sub>1 \<Longrightarrow>
+  \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s\<close>.  Multiple results are considered as
   error (exception @{ML THM}).
 
-  \<^descr> @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
-  (thm\<^sub>1, 1, thm\<^sub>2)"}.
+  \<^descr> \<open>thm\<^sub>1 COMP thm\<^sub>2\<close> is the same as \<open>Drule.compose
+  (thm\<^sub>1, 1, thm\<^sub>2)\<close>.
 
 
   \begin{warn}
@@ -554,42 +540,35 @@
   @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
-  composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a goal
+  \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op THEN}~\<open>tac\<^sub>2\<close> is the sequential
+  composition of \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>.  Applied to a goal
   state, it returns all states reachable in two steps by applying
-  @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it applies @{text
-  "tac\<^sub>1"} to the goal state, getting a sequence of possible next
-  states; then, it applies @{text "tac\<^sub>2"} to each of these and
+  \<open>tac\<^sub>1\<close> followed by \<open>tac\<^sub>2\<close>.  First, it applies \<open>tac\<^sub>1\<close> to the goal state, getting a sequence of possible next
+  states; then, it applies \<open>tac\<^sub>2\<close> to each of these and
   concatenates the results to produce again one flat sequence of
   states.
 
-  \<^descr> @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
-  between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it
-  tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text
-  "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}.  This is a deterministic
-  choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded
+  \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op ORELSE}~\<open>tac\<^sub>2\<close> makes a choice
+  between \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>.  Applied to a state, it
+  tries \<open>tac\<^sub>1\<close> and returns the result if non-empty; if \<open>tac\<^sub>1\<close> fails then it uses \<open>tac\<^sub>2\<close>.  This is a deterministic
+  choice: if \<open>tac\<^sub>1\<close> succeeds then \<open>tac\<^sub>2\<close> is excluded
   from the result.
 
-  \<^descr> @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the
-  possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Unlike
+  \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op APPEND}~\<open>tac\<^sub>2\<close> concatenates the
+  possible results of \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>.  Unlike
   @{ML_op "ORELSE"} there is \<^emph>\<open>no commitment\<close> to either tactic, so
   @{ML_op "APPEND"} helps to avoid incompleteness during search, at
   the cost of potential inefficiencies.
 
-  \<^descr> @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
-  "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.
+  \<^descr> @{ML EVERY}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op THEN}~\<open>tac\<^sub>n\<close>.
   Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always
   succeeds.
 
-  \<^descr> @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
-  "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text
-  "tac\<^sub>n"}.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
+  \<^descr> @{ML FIRST}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op "ORELSE"}~\<open>tac\<^sub>n\<close>.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
   always fails.
 
   \<^descr> @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
-  tactics with explicit subgoal addressing.  So @{text
-  "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
-  "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
+  tactics with explicit subgoal addressing.  So \<open>(tac\<^sub>1\<close>~@{ML_op THEN'}~\<open>tac\<^sub>2) i\<close> is the same as \<open>(tac\<^sub>1 i\<close>~@{ML_op THEN}~\<open>tac\<^sub>2 i)\<close>.
 
   The other primed tacticals work analogously.
 \<close>
@@ -610,35 +589,33 @@
   @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
+  \<^descr> @{ML TRY}~\<open>tac\<close> applies \<open>tac\<close> to the goal
   state and returns the resulting sequence, if non-empty; otherwise it
-  returns the original state.  Thus, it applies @{text "tac"} at most
+  returns the original state.  Thus, it applies \<open>tac\<close> at most
   once.
 
   Note that for tactics with subgoal addressing, the combinator can be
-  applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
-  "tac"}.  There is no need for @{verbatim TRY'}.
+  applied via functional composition: @{ML "TRY"}~@{ML_op o}~\<open>tac\<close>.  There is no need for @{verbatim TRY'}.
 
-  \<^descr> @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal
+  \<^descr> @{ML REPEAT}~\<open>tac\<close> applies \<open>tac\<close> to the goal
   state and, recursively, to each element of the resulting sequence.
-  The resulting sequence consists of those states that make @{text
-  "tac"} fail.  Thus, it applies @{text "tac"} as many times as
+  The resulting sequence consists of those states that make \<open>tac\<close> fail.  Thus, it applies \<open>tac\<close> as many times as
   possible (including zero times), and allows backtracking over each
-  invocation of @{text "tac"}.  @{ML REPEAT} is more general than @{ML
+  invocation of \<open>tac\<close>.  @{ML REPEAT} is more general than @{ML
   REPEAT_DETERM}, but requires more space.
 
-  \<^descr> @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}
-  but it always applies @{text "tac"} at least once, failing if this
+  \<^descr> @{ML REPEAT1}~\<open>tac\<close> is like @{ML REPEAT}~\<open>tac\<close>
+  but it always applies \<open>tac\<close> at least once, failing if this
   is impossible.
 
-  \<^descr> @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
+  \<^descr> @{ML REPEAT_DETERM}~\<open>tac\<close> applies \<open>tac\<close> to the
   goal state and, recursively, to the head of the resulting sequence.
-  It returns the first state to make @{text "tac"} fail.  It is
+  It returns the first state to make \<open>tac\<close> fail.  It is
   deterministic, discarding alternative outcomes.
 
-  \<^descr> @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
-  REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
-  by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
+  \<^descr> @{ML REPEAT_DETERM_N}~\<open>n tac\<close> is like @{ML
+  REPEAT_DETERM}~\<open>tac\<close> but the number of repetitions is bound
+  by \<open>n\<close> (where @{ML "~1"} means \<open>\<infinity>\<close>).
 \<close>
 
 text %mlex \<open>The basic tactics and tacticals considered above follow
@@ -649,7 +626,7 @@
 
   \<^item> @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
   @{ML_op "APPEND"}.  Also, it is a zero element for @{ML_op "THEN"},
-  which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
+  which means that \<open>tac\<close>~@{ML_op THEN}~@{ML no_tac} is
   equivalent to @{ML no_tac}.
 
   \<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
@@ -662,9 +639,9 @@
   fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;
 \<close>
 
-text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML
-  REPEAT}~@{text "tac"}.  @{ML REPEAT} uses @{ML_op "ORELSE"} and not
-  @{ML_op "APPEND"}, it applies @{text "tac"} as many times as
+text \<open>If \<open>tac\<close> can return multiple outcomes then so can @{ML
+  REPEAT}~\<open>tac\<close>.  @{ML REPEAT} uses @{ML_op "ORELSE"} and not
+  @{ML_op "APPEND"}, it applies \<open>tac\<close> as many times as
   possible in each outcome.
 
   \begin{warn}
@@ -672,7 +649,7 @@
   definition of @{ML REPEAT}.  Recursive tacticals must be coded in
   this awkward fashion to avoid infinite recursion of eager functional
   evaluation in Standard ML.  The following attempt would make @{ML
-  REPEAT}~@{text "tac"} loop:
+  REPEAT}~\<open>tac\<close> loop:
   \end{warn}
 \<close>
 
@@ -690,9 +667,9 @@
   tactic a certain range of subgoals is covered.  Thus the body tactic
   is applied to \<^emph>\<open>all\<close> subgoals, \<^emph>\<open>some\<close> subgoal etc.
 
-  Suppose that the goal state has @{text "n \<ge> 0"} subgoals.  Many of
+  Suppose that the goal state has \<open>n \<ge> 0\<close> subgoals.  Many of
   these tacticals address subgoal ranges counting downwards from
-  @{text "n"} towards @{text "1"}.  This has the fortunate effect that
+  \<open>n\<close> towards \<open>1\<close>.  This has the fortunate effect that
   newly emerging subgoals are concatenated in the result, without
   interfering each other.  Nonetheless, there might be situations
   where a different order is desired.\<close>
@@ -708,30 +685,30 @@
   @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
-  n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}.  It
-  applies the @{text tac} to all the subgoals, counting downwards.
+  \<^descr> @{ML ALLGOALS}~\<open>tac\<close> is equivalent to \<open>tac
+  n\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op THEN}~\<open>tac 1\<close>.  It
+  applies the \<open>tac\<close> to all the subgoals, counting downwards.
 
-  \<^descr> @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac
-  n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}.  It
-  applies @{text "tac"} to one subgoal, counting downwards.
+  \<^descr> @{ML SOMEGOAL}~\<open>tac\<close> is equivalent to \<open>tac
+  n\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op ORELSE}~\<open>tac 1\<close>.  It
+  applies \<open>tac\<close> to one subgoal, counting downwards.
 
-  \<^descr> @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac
-  1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}.  It
-  applies @{text "tac"} to one subgoal, counting upwards.
+  \<^descr> @{ML FIRSTGOAL}~\<open>tac\<close> is equivalent to \<open>tac
+  1\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op ORELSE}~\<open>tac n\<close>.  It
+  applies \<open>tac\<close> to one subgoal, counting upwards.
 
-  \<^descr> @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
-  It applies @{text "tac"} unconditionally to the first subgoal.
+  \<^descr> @{ML HEADGOAL}~\<open>tac\<close> is equivalent to \<open>tac 1\<close>.
+  It applies \<open>tac\<close> unconditionally to the first subgoal.
 
-  \<^descr> @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
+  \<^descr> @{ML REPEAT_SOME}~\<open>tac\<close> applies \<open>tac\<close> once or
   more to a subgoal, counting downwards.
 
-  \<^descr> @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
+  \<^descr> @{ML REPEAT_FIRST}~\<open>tac\<close> applies \<open>tac\<close> once or
   more to a subgoal, counting upwards.
 
-  \<^descr> @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to
-  @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
-  THEN}~@{text "tac\<^sub>1 i"}.  It applies the given list of tactics to the
+  \<^descr> @{ML RANGE}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>k] i\<close> is equivalent to
+  \<open>tac\<^sub>k (i + k - 1)\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op
+  THEN}~\<open>tac\<^sub>1 i\<close>.  It applies the given list of tactics to the
   corresponding range of subgoals, counting downwards.
 \<close>
 
@@ -757,14 +734,14 @@
   @{index_ML CHANGED: "tactic -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
+  \<^descr> @{ML FILTER}~\<open>sat tac\<close> applies \<open>tac\<close> to the
   goal state and returns a sequence consisting of those result goal
-  states that are satisfactory in the sense of @{text "sat"}.
+  states that are satisfactory in the sense of \<open>sat\<close>.
 
-  \<^descr> @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal
+  \<^descr> @{ML CHANGED}~\<open>tac\<close> applies \<open>tac\<close> to the goal
   state and returns precisely those states that differ from the
   original state (according to @{ML Thm.eq_thm}).  Thus @{ML
-  CHANGED}~@{text "tac"} always has some effect on the state.
+  CHANGED}~\<open>tac\<close> always has some effect on the state.
 \<close>
 
 
@@ -777,17 +754,17 @@
   @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
-  @{text "sat"} returns true.  Otherwise it applies @{text "tac"},
+  \<^descr> @{ML DEPTH_FIRST}~\<open>sat tac\<close> returns the goal state if
+  \<open>sat\<close> returns true.  Otherwise it applies \<open>tac\<close>,
   then recursively searches from each element of the resulting
   sequence.  The code uses a stack for efficiency, in effect applying
-  @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to
+  \<open>tac\<close>~@{ML_op THEN}~@{ML DEPTH_FIRST}~\<open>sat tac\<close> to
   the state.
 
-  \<^descr> @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
+  \<^descr> @{ML DEPTH_SOLVE}\<open>tac\<close> uses @{ML DEPTH_FIRST} to
   search for states having no subgoals.
 
-  \<^descr> @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
+  \<^descr> @{ML DEPTH_SOLVE_1}~\<open>tac\<close> uses @{ML DEPTH_FIRST} to
   search for states having fewer subgoals than the given state.  Thus,
   it insists upon solving at least one subgoal.
 \<close>
@@ -804,16 +781,16 @@
 
   These search strategies will find a solution if one exists.
   However, they do not enumerate all solutions; they terminate after
-  the first satisfactory result from @{text "tac"}.
+  the first satisfactory result from \<open>tac\<close>.
 
-  \<^descr> @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
-  search to find states for which @{text "sat"} is true.  For most
+  \<^descr> @{ML BREADTH_FIRST}~\<open>sat tac\<close> uses breadth-first
+  search to find states for which \<open>sat\<close> is true.  For most
   applications, it is too slow.
 
-  \<^descr> @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic
-  search, using @{text "dist"} to estimate the distance from a
-  satisfactory state (in the sense of @{text "sat"}).  It maintains a
-  list of states ordered by distance.  It applies @{text "tac"} to the
+  \<^descr> @{ML BEST_FIRST}~\<open>(sat, dist) tac\<close> does a heuristic
+  search, using \<open>dist\<close> to estimate the distance from a
+  satisfactory state (in the sense of \<open>sat\<close>).  It maintains a
+  list of states ordered by distance.  It applies \<open>tac\<close> to the
   head of this list; if the result contains any satisfactory states,
   then it returns them.  Otherwise, @{ML BEST_FIRST} adds the new
   states to the list, and continues.
@@ -822,9 +799,9 @@
   the size of the state.  The smaller the state, the fewer and simpler
   subgoals it has.
 
-  \<^descr> @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like
+  \<^descr> @{ML THEN_BEST_FIRST}~\<open>tac\<^sub>0 (sat, dist) tac\<close> is like
   @{ML BEST_FIRST}, except that the priority queue initially contains
-  the result of applying @{text "tac\<^sub>0"} to the goal state.  This
+  the result of applying \<open>tac\<^sub>0\<close> to the goal state.  This
   tactical permits separate tactics for starting the search and
   continuing the search.
 \<close>
@@ -840,22 +817,22 @@
   @{index_ML DETERM: "tactic -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to
-  the goal state if it satisfies predicate @{text "sat"}, and applies
-  @{text "tac\<^sub>2"}.  It is a conditional tactical in that only one of
-  @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.
-  However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated
+  \<^descr> @{ML COND}~\<open>sat tac\<^sub>1 tac\<^sub>2\<close> applies \<open>tac\<^sub>1\<close> to
+  the goal state if it satisfies predicate \<open>sat\<close>, and applies
+  \<open>tac\<^sub>2\<close>.  It is a conditional tactical in that only one of
+  \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close> is applied to a goal state.
+  However, both \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close> are evaluated
   because ML uses eager evaluation.
 
-  \<^descr> @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the
+  \<^descr> @{ML IF_UNSOLVED}~\<open>tac\<close> applies \<open>tac\<close> to the
   goal state if it has any subgoals, and simply returns the goal state
   otherwise.  Many common tactics, such as @{ML resolve_tac}, fail if
   applied to a goal state that has no subgoals.
 
-  \<^descr> @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
+  \<^descr> @{ML SOLVE}~\<open>tac\<close> applies \<open>tac\<close> to the goal
   state and then fails iff there are subgoals left.
 
-  \<^descr> @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
+  \<^descr> @{ML DETERM}~\<open>tac\<close> applies \<open>tac\<close> to the goal
   state and returns the head of the resulting sequence.  @{ML DETERM}
   limits the search space by making its argument deterministic.
 \<close>
@@ -871,20 +848,17 @@
   @{index_ML size_of_thm: "thm -> int"} \\
   \end{mldecls}
 
-  \<^descr> @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
-  "thm"} has fewer than @{text "n"} premises.
+  \<^descr> @{ML has_fewer_prems}~\<open>n thm\<close> reports whether \<open>thm\<close> has fewer than \<open>n\<close> premises.
 
-  \<^descr> @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
-  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
+  \<^descr> @{ML Thm.eq_thm}~\<open>(thm\<^sub>1, thm\<^sub>2)\<close> reports whether \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> are equal.  Both theorems must have the
   same conclusions, the same set of hypotheses, and the same set of sort
   hypotheses.  Names of bound variables are ignored as usual.
 
-  \<^descr> @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
-  the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.
+  \<^descr> @{ML Thm.eq_thm_prop}~\<open>(thm\<^sub>1, thm\<^sub>2)\<close> reports whether
+  the propositions of \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> are equal.
   Names of bound variables are ignored.
 
-  \<^descr> @{ML size_of_thm}~@{text "thm"} computes the size of @{text
-  "thm"}, namely the number of variables, constants and abstractions
+  \<^descr> @{ML size_of_thm}~\<open>thm\<close> computes the size of \<open>thm\<close>, namely the number of variables, constants and abstractions
   in its conclusion.  It may serve as a distance function for
   @{ML BEST_FIRST}.
 \<close>