# HG changeset patch
# User wenzelm
# Date 1458205177 -3600
# Node ID 47635cd9a996a79314ce24e5ebf0696a03ed57ae
# Parent  1d1d7f5c0b277b48ae33f2ceafbc3223d9bd0929
tuned whitespace;

diff -r 1d1d7f5c0b27 -r 47635cd9a996 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 09:41:21 2016 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Thu Mar 17 09:59:37 2016 +0100
@@ -247,24 +247,23 @@
 
 section \<open>The Simplifier \label{sec:simplifier}\<close>
 
-text \<open>The Simplifier performs conditional and unconditional
-  rewriting and uses contextual information: rule declarations in the
-  background theory or local proof context are taken into account, as
-  well as chained facts and subgoal premises (``local assumptions'').
-  There are several general hooks that allow to modify the
-  simplification strategy, or incorporate other proof tools that solve
-  sub-problems, produce rewrite rules on demand etc.
+text \<open>
+  The Simplifier performs conditional and unconditional rewriting and uses
+  contextual information: rule declarations in the background theory or local
+  proof context are taken into account, as well as chained facts and subgoal
+  premises (``local assumptions''). There are several general hooks that allow
+  to modify the simplification strategy, or incorporate other proof tools that
+  solve sub-problems, produce rewrite rules on demand etc.
 
-  The rewriting strategy is always strictly bottom up, except for
-  congruence rules, which are applied while descending into a term.
-  Conditions in conditional rewrite rules are solved recursively
-  before the rewrite rule is applied.
+  The rewriting strategy is always strictly bottom up, except for congruence
+  rules, which are applied while descending into a term. Conditions in
+  conditional rewrite rules are solved recursively before the rewrite rule is
+  applied.
 
-  The default Simplifier setup of major object logics (HOL, HOLCF,
-  FOL, ZF) makes the Simplifier ready for immediate use, without
-  engaging into the internal structures.  Thus it serves as
-  general-purpose proof tool with the main focus on equational
-  reasoning, and a bit more than that.
+  The default Simplifier setup of major object logics (HOL, HOLCF, FOL, ZF)
+  makes the Simplifier ready for immediate use, without engaging into the
+  internal structures. Thus it serves as general-purpose proof tool with the
+  main focus on equational reasoning, and a bit more than that.
 \<close>
 
 
@@ -288,69 +287,63 @@
       'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   \<close>}
 
-  \<^descr> @{method simp} invokes the Simplifier on the first subgoal,
-  after inserting chained facts as additional goal premises; further
-  rule declarations may be included via \<open>(simp add: facts)\<close>.
-  The proof method fails if the subgoal remains unchanged after
-  simplification.
+  \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
+  inserting chained facts as additional goal premises; further rule
+  declarations may be included via \<open>(simp add: facts)\<close>. The proof method fails
+  if the subgoal remains unchanged after simplification.
 
-  Note that the original goal premises and chained facts are subject
-  to simplification themselves, while declarations via \<open>add\<close>/\<open>del\<close> merely follow the policies of the object-logic
-  to extract rewrite rules from theorems, without further
-  simplification.  This may lead to slightly different behavior in
-  either case, which might be required precisely like that in some
-  boundary situations to perform the intended simplification step!
+  Note that the original goal premises and chained facts are subject to
+  simplification themselves, while declarations via \<open>add\<close>/\<open>del\<close> merely follow
+  the policies of the object-logic to extract rewrite rules from theorems,
+  without further simplification. This may lead to slightly different behavior
+  in either case, which might be required precisely like that in some boundary
+  situations to perform the intended simplification step!
 
   \<^medskip>
-  The \<open>only\<close> modifier first removes all other rewrite
-  rules, looper tactics (including split rules), congruence rules, and
-  then behaves like \<open>add\<close>.  Implicit solvers remain, which means
-  that trivial rules like reflexivity or introduction of \<open>True\<close> are available to solve the simplified subgoals, but also
-  non-trivial tools like linear arithmetic in HOL.  The latter may
-  lead to some surprise of the meaning of ``only'' in Isabelle/HOL
-  compared to English!
+  The \<open>only\<close> modifier first removes all other rewrite rules, looper tactics
+  (including split rules), congruence rules, and then behaves like \<open>add\<close>.
+  Implicit solvers remain, which means that trivial rules like reflexivity or
+  introduction of \<open>True\<close> are available to solve the simplified subgoals, but
+  also non-trivial tools like linear arithmetic in HOL. The latter may lead to
+  some surprise of the meaning of ``only'' in Isabelle/HOL compared to
+  English!
 
   \<^medskip>
-  The \<open>split\<close> modifiers add or delete rules for the
-  Splitter (see also \secref{sec:simp-strategies} on the looper).
-  This works only if the Simplifier method has been properly setup to
-  include the Splitter (all major object logics such HOL, HOLCF, FOL,
-  ZF do this already).
+  The \<open>split\<close> modifiers add or delete rules for the Splitter (see also
+  \secref{sec:simp-strategies} on the looper). This works only if the
+  Simplifier method has been properly setup to include the Splitter (all major
+  object logics such HOL, HOLCF, FOL, ZF do this already).
 
   There is also a separate @{method_ref split} method available for
-  single-step case splitting.  The effect of repeatedly applying
-  \<open>(split thms)\<close> can be imitated by ``\<open>(simp only:
-  split: thms)\<close>''.
+  single-step case splitting. The effect of repeatedly applying \<open>(split thms)\<close>
+  can be imitated by ``\<open>(simp only: split: thms)\<close>''.
 
   \<^medskip>
-  The \<open>cong\<close> modifiers add or delete Simplifier
-  congruence rules (see also \secref{sec:simp-rules}); the default is
-  to add.
+  The \<open>cong\<close> modifiers add or delete Simplifier congruence rules (see also
+  \secref{sec:simp-rules}); the default is to add.
 
-  \<^descr> @{method simp_all} is similar to @{method simp}, but acts on
-  all goals, working backwards from the last to the first one as usual
-  in Isabelle.\<^footnote>\<open>The order is irrelevant for goals without
-  schematic variables, so simplification might actually be performed
-  in parallel here.\<close>
+  \<^descr> @{method simp_all} is similar to @{method simp}, but acts on all goals,
+  working backwards from the last to the first one as usual in Isabelle.\<^footnote>\<open>The
+  order is irrelevant for goals without schematic variables, so simplification
+  might actually be performed in parallel here.\<close>
 
-  Chained facts are inserted into all subgoals, before the
-  simplification process starts.  Further rule declarations are the
-  same as for @{method simp}.
+  Chained facts are inserted into all subgoals, before the simplification
+  process starts. Further rule declarations are the same as for @{method
+  simp}.
 
   The proof method fails if all subgoals remain unchanged after
   simplification.
 
-  \<^descr> @{attribute simp_depth_limit} limits the number of recursive
-  invocations of the Simplifier during conditional rewriting.
+  \<^descr> @{attribute simp_depth_limit} limits the number of recursive invocations
+  of the Simplifier during conditional rewriting.
 
 
-  By default the Simplifier methods above take local assumptions fully
-  into account, using equational assumptions in the subsequent
-  normalization process, or simplifying assumptions themselves.
-  Further options allow to fine-tune the behavior of the Simplifier
-  in this respect, corresponding to a variety of ML tactics as
-  follows.\<^footnote>\<open>Unlike the corresponding Isar proof methods, the
-  ML tactics do not insist in changing the goal state.\<close>
+  By default the Simplifier methods above take local assumptions fully into
+  account, using equational assumptions in the subsequent normalization
+  process, or simplifying assumptions themselves. Further options allow to
+  fine-tune the behavior of the Simplifier in this respect, corresponding to a
+  variety of ML tactics as follows.\<^footnote>\<open>Unlike the corresponding Isar proof
+  methods, the ML tactics do not insist in changing the goal state.\<close>
 
   \begin{center}
   \small
@@ -358,24 +351,21 @@
   \hline
   Isar method & ML tactic & behavior \\\hline
 
-  \<open>(simp (no_asm))\<close> & @{ML simp_tac} & assumptions are ignored
-  completely \\\hline
+  \<open>(simp (no_asm))\<close> & @{ML simp_tac} & assumptions are ignored completely
+  \\\hline
 
-  \<open>(simp (no_asm_simp))\<close> & @{ML asm_simp_tac} & assumptions
-  are used in the simplification of the conclusion but are not
-  themselves simplified \\\hline
+  \<open>(simp (no_asm_simp))\<close> & @{ML asm_simp_tac} & assumptions are used in the
+  simplification of the conclusion but are not themselves simplified \\\hline
 
-  \<open>(simp (no_asm_use))\<close> & @{ML full_simp_tac} & assumptions
-  are simplified but are not used in the simplification of each other
-  or the conclusion \\\hline
+  \<open>(simp (no_asm_use))\<close> & @{ML full_simp_tac} & assumptions are simplified but
+  are not used in the simplification of each other or the conclusion \\\hline
 
-  \<open>(simp)\<close> & @{ML asm_full_simp_tac} & assumptions are used in
-  the simplification of the conclusion and to simplify other
-  assumptions \\\hline
+  \<open>(simp)\<close> & @{ML asm_full_simp_tac} & assumptions are used in the
+  simplification of the conclusion and to simplify other assumptions \\\hline
 
-  \<open>(simp (asm_lr))\<close> & @{ML asm_lr_simp_tac} & compatibility
-  mode: an assumption is only used for simplifying assumptions which
-  are to the right of it \\\hline
+  \<open>(simp (asm_lr))\<close> & @{ML asm_lr_simp_tac} & compatibility mode: an
+  assumption is only used for simplifying assumptions which are to the right
+  of it \\\hline
 
   \end{tabular}
   \end{center}
@@ -384,18 +374,19 @@
 
 subsubsection \<open>Examples\<close>
 
-text \<open>We consider basic algebraic simplifications in Isabelle/HOL.
-  The rather trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like
-  a good candidate to be solved by a single call of @{method simp}:
+text \<open>
+  We consider basic algebraic simplifications in Isabelle/HOL. The rather
+  trivial goal @{prop "0 + (x + 0) = x + 0 + 0"} looks like a good candidate
+  to be solved by a single call of @{method simp}:
 \<close>
 
 lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
 
-text \<open>The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term
-  "op +"} in the HOL library are declared as generic type class
-  operations, without stating any algebraic laws yet.  More specific
-  types are required to get access to certain standard simplifications
-  of the theory context, e.g.\ like this:\<close>
+text \<open>
+  The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term "op +"} in the
+  HOL library are declared as generic type class operations, without stating
+  any algebraic laws yet. More specific types are required to get access to
+  certain standard simplifications of the theory context, e.g.\ like this:\<close>
 
 lemma fixes x :: nat shows "0 + (x + 0) = x + 0 + 0" by simp
 lemma fixes x :: int shows "0 + (x + 0) = x + 0 + 0" by simp
@@ -403,39 +394,38 @@
 
 text \<open>
   \<^medskip>
-  In many cases, assumptions of a subgoal are also needed in
-  the simplification process.  For example:
+  In many cases, assumptions of a subgoal are also needed in the
+  simplification process. For example:
 \<close>
 
 lemma fixes x :: nat shows "x = 0 \<Longrightarrow> x + x = 0" by simp
 lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" apply simp oops
 lemma fixes x :: nat assumes "x = 0" shows "x + x = 0" using assms by simp
 
-text \<open>As seen above, local assumptions that shall contribute to
-  simplification need to be part of the subgoal already, or indicated
-  explicitly for use by the subsequent method invocation.  Both too
-  little or too much information can make simplification fail, for
-  different reasons.
+text \<open>
+  As seen above, local assumptions that shall contribute to simplification
+  need to be part of the subgoal already, or indicated explicitly for use by
+  the subsequent method invocation. Both too little or too much information
+  can make simplification fail, for different reasons.
 
-  In the next example the malicious assumption @{prop "\<And>x::nat. f x =
-  g (f (g x))"} does not contribute to solve the problem, but makes
-  the default @{method simp} method loop: the rewrite rule \<open>f
-  ?x \<equiv> g (f (g ?x))\<close> extracted from the assumption does not
-  terminate.  The Simplifier notices certain simple forms of
-  nontermination, but not this one.  The problem can be solved
-  nonetheless, by ignoring assumptions via special options as
-  explained before:
+  In the next example the malicious assumption @{prop "\<And>x::nat. f x = g (f (g
+  x))"} does not contribute to solve the problem, but makes the default
+  @{method simp} method loop: the rewrite rule \<open>f ?x \<equiv> g (f (g ?x))\<close> extracted
+  from the assumption does not terminate. The Simplifier notices certain
+  simple forms of nontermination, but not this one. The problem can be solved
+  nonetheless, by ignoring assumptions via special options as explained
+  before:
 \<close>
 
 lemma "(\<And>x::nat. f x = g (f (g x))) \<Longrightarrow> f 0 = f 0 + 0"
   by (simp (no_asm))
 
-text \<open>The latter form is typical for long unstructured proof
-  scripts, where the control over the goal content is limited.  In
-  structured proofs it is usually better to avoid pushing too many
-  facts into the goal state in the first place.  Assumptions in the
-  Isar proof context do not intrude the reasoning if not used
-  explicitly.  This is illustrated for a toplevel statement and a
+text \<open>
+  The latter form is typical for long unstructured proof scripts, where the
+  control over the goal content is limited. In structured proofs it is usually
+  better to avoid pushing too many facts into the goal state in the first
+  place. Assumptions in the Isar proof context do not intrude the reasoning if
+  not used explicitly. This is illustrated for a toplevel statement and a
   local proof body as follows:
 \<close>
 
@@ -451,26 +441,26 @@
 
 text \<open>
   \<^medskip>
-  Because assumptions may simplify each other, there
-  can be very subtle cases of nontermination. For example, the regular
-  @{method simp} method applied to @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y
-  \<Longrightarrow> Q"} gives rise to the infinite reduction sequence
+  Because assumptions may simplify each other, there can be very subtle cases
+  of nontermination. For example, the regular @{method simp} method applied to
+  @{prop "P (f x) \<Longrightarrow> y = x \<Longrightarrow> f x = f y \<Longrightarrow> Q"} gives rise to the infinite
+  reduction sequence
   \[
   \<open>P (f x)\<close> \stackrel{\<open>f x \<equiv> f y\<close>}{\longmapsto}
   \<open>P (f y)\<close> \stackrel{\<open>y \<equiv> x\<close>}{\longmapsto}
   \<open>P (f x)\<close> \stackrel{\<open>f x \<equiv> f y\<close>}{\longmapsto} \cdots
   \]
-  whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow>
-  Q"} terminates (without solving the goal):
+  whereas applying the same to @{prop "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"}
+  terminates (without solving the goal):
 \<close>
 
 lemma "y = x \<Longrightarrow> f x = f y \<Longrightarrow> P (f x) \<Longrightarrow> Q"
   apply simp
   oops
 
-text \<open>See also \secref{sec:simp-trace} for options to enable
-  Simplifier trace mode, which often helps to diagnose problems with
-  rewrite systems.
+text \<open>
+  See also \secref{sec:simp-trace} for options to enable Simplifier trace
+  mode, which often helps to diagnose problems with rewrite systems.
 \<close>
 
 
@@ -491,200 +481,191 @@
     @@{command print_simpset} ('!'?)
   \<close>}
 
-  \<^descr> @{attribute simp} declares rewrite rules, by adding or
-  deleting them from the simpset within the theory or proof context.
-  Rewrite rules are theorems expressing some form of equality, for
-  example:
+  \<^descr> @{attribute simp} declares rewrite rules, by adding or deleting them from
+  the simpset within the theory or proof context. Rewrite rules are theorems
+  expressing some form of equality, for example:
 
   \<open>Suc ?m + ?n = ?m + Suc ?n\<close> \\
   \<open>?P \<and> ?P \<longleftrightarrow> ?P\<close> \\
   \<open>?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}\<close>
 
   \<^medskip>
-  Conditional rewrites such as \<open>?m < ?n \<Longrightarrow> ?m div ?n = 0\<close> are
-  also permitted; the conditions can be arbitrary formulas.
+  Conditional rewrites such as \<open>?m < ?n \<Longrightarrow> ?m div ?n = 0\<close> are also permitted;
+  the conditions can be arbitrary formulas.
 
   \<^medskip>
-  Internally, all rewrite rules are translated into Pure
-  equalities, theorems with conclusion \<open>lhs \<equiv> rhs\<close>. The
-  simpset contains a function for extracting equalities from arbitrary
-  theorems, which is usually installed when the object-logic is
-  configured initially. For example, \<open>\<not> ?x \<in> {}\<close> could be
-  turned into \<open>?x \<in> {} \<equiv> False\<close>. Theorems that are declared as
-  @{attribute simp} and local assumptions within a goal are treated
-  uniformly in this respect.
+  Internally, all rewrite rules are translated into Pure equalities, theorems
+  with conclusion \<open>lhs \<equiv> rhs\<close>. The simpset contains a function for extracting
+  equalities from arbitrary theorems, which is usually installed when the
+  object-logic is configured initially. For example, \<open>\<not> ?x \<in> {}\<close> could be
+  turned into \<open>?x \<in> {} \<equiv> False\<close>. Theorems that are declared as @{attribute
+  simp} and local assumptions within a goal are treated uniformly in this
+  respect.
 
-  The Simplifier accepts the following formats for the \<open>lhs\<close>
-  term:
+  The Simplifier accepts the following formats for the \<open>lhs\<close> term:
 
-    \<^enum> First-order patterns, considering the sublanguage of
-    application of constant operators to variable operands, without
-    \<open>\<lambda>\<close>-abstractions or functional variables.
-    For example:
+    \<^enum> First-order patterns, considering the sublanguage of application of
+    constant operators to variable operands, without \<open>\<lambda>\<close>-abstractions or
+    functional variables. For example:
 
     \<open>(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)\<close> \\
     \<open>f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)\<close>
 
-    \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
-    These are terms in \<open>\<beta>\<close>-normal form (this will always be the
-    case unless you have done something strange) where each occurrence
-    of an unknown is of the form \<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the
-    \<open>x\<^sub>i\<close> are distinct bound variables.
+    \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}. These
+    are terms in \<open>\<beta>\<close>-normal form (this will always be the case unless you have
+    done something strange) where each occurrence of an unknown is of the form
+    \<open>?F x\<^sub>1 \<dots> x\<^sub>n\<close>, where the \<open>x\<^sub>i\<close> are distinct bound variables.
 
-    For example, \<open>(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)\<close>
-    or its symmetric form, since the \<open>rhs\<close> is also a
-    higher-order pattern.
+    For example, \<open>(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)\<close> or its
+    symmetric form, since the \<open>rhs\<close> is also a higher-order pattern.
 
-    \<^enum> Physical first-order patterns over raw \<open>\<lambda>\<close>-term
-    structure without \<open>\<alpha>\<beta>\<eta>\<close>-equality; abstractions and bound
-    variables are treated like quasi-constant term material.
+    \<^enum> Physical first-order patterns over raw \<open>\<lambda>\<close>-term structure without
+    \<open>\<alpha>\<beta>\<eta>\<close>-equality; abstractions and bound variables are treated like
+    quasi-constant term material.
 
-    For example, the rule \<open>?f ?x \<in> range ?f = True\<close> rewrites the
-    term \<open>g a \<in> range g\<close> to \<open>True\<close>, but will fail to
-    match \<open>g (h b) \<in> range (\<lambda>x. g (h x))\<close>. However, offending
-    subterms (in our case \<open>?f ?x\<close>, which is not a pattern) can
-    be replaced by adding new variables and conditions like this: \<open>?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True\<close> is acceptable as a conditional
-    rewrite rule of the second category since conditions can be
-    arbitrary terms.
+    For example, the rule \<open>?f ?x \<in> range ?f = True\<close> rewrites the term \<open>g a \<in>
+    range g\<close> to \<open>True\<close>, but will fail to match \<open>g (h b) \<in> range (\<lambda>x. g (h
+    x))\<close>. However, offending subterms (in our case \<open>?f ?x\<close>, which is not a
+    pattern) can be replaced by adding new variables and conditions like this:
+    \<open>?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True\<close> is acceptable as a conditional rewrite
+    rule of the second category since conditions can be arbitrary terms.
 
   \<^descr> @{attribute split} declares case split rules.
 
-  \<^descr> @{attribute cong} declares congruence rules to the Simplifier
-  context.
+  \<^descr> @{attribute cong} declares congruence rules to the Simplifier context.
 
   Congruence rules are equalities of the form @{text [display]
   "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
 
-  This controls the simplification of the arguments of \<open>f\<close>.  For
-  example, some arguments can be simplified under additional
-  assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
-  (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
+  This controls the simplification of the arguments of \<open>f\<close>. For example, some
+  arguments can be simplified under additional assumptions:
+  @{text [display]
+    "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow>
+    (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow>
+    (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"}
 
-  Given this rule, the Simplifier assumes \<open>?Q\<^sub>1\<close> and extracts
-  rewrite rules from it when simplifying \<open>?P\<^sub>2\<close>.  Such local
-  assumptions are effective for rewriting formulae such as \<open>x =
-  0 \<longrightarrow> y + x = y\<close>.
+  Given this rule, the Simplifier assumes \<open>?Q\<^sub>1\<close> and extracts rewrite rules
+  from it when simplifying \<open>?P\<^sub>2\<close>. Such local assumptions are effective for
+  rewriting formulae such as \<open>x = 0 \<longrightarrow> y + x = y\<close>.
 
   %FIXME
   %The local assumptions are also provided as theorems to the solver;
   %see \secref{sec:simp-solver} below.
 
   \<^medskip>
-  The following congruence rule for bounded quantifiers also
-  supplies contextual information --- about the bound variable:
-  @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
+  The following congruence rule for bounded quantifiers also supplies
+  contextual information --- about the bound variable: @{text [display]
+  "(?A = ?B) \<Longrightarrow>
+    (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow>
     (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"}
 
   \<^medskip>
-  This congruence rule for conditional expressions can
-  supply contextual information for simplifying the arms:
-  @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
+  This congruence rule for conditional expressions can supply contextual
+  information for simplifying the arms: @{text [display]
+  "?p = ?q \<Longrightarrow>
+    (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow>
+    (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow>
     (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"}
 
-  A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some
-  arguments.  Here is an alternative congruence rule for conditional
-  expressions that conforms to non-strict functional evaluation:
-  @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
+  A congruence rule can also \<^emph>\<open>prevent\<close> simplification of some arguments. Here
+  is an alternative congruence rule for conditional expressions that conforms
+  to non-strict functional evaluation: @{text [display]
+  "?p = ?q \<Longrightarrow>
+    (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"}
 
-  Only the first argument is simplified; the others remain unchanged.
-  This can make simplification much faster, but may require an extra
-  case split over the condition \<open>?q\<close> to prove the goal.
+  Only the first argument is simplified; the others remain unchanged. This can
+  make simplification much faster, but may require an extra case split over
+  the condition \<open>?q\<close> to prove the goal.
 
-  \<^descr> @{command "print_simpset"} prints the collection of rules declared
-  to the Simplifier, which is also known as ``simpset'' internally; the
-  ``\<open>!\<close>'' option indicates extra verbosity.
+  \<^descr> @{command "print_simpset"} prints the collection of rules declared to the
+  Simplifier, which is also known as ``simpset'' internally; the ``\<open>!\<close>''
+  option indicates extra verbosity.
 
-  For historical reasons, simpsets may occur independently from the
-  current context, but are conceptually dependent on it.  When the
-  Simplifier is invoked via one of its main entry points in the Isar
-  source language (as proof method \secref{sec:simp-meth} or rule
-  attribute \secref{sec:simp-meth}), its simpset is derived from the
-  current proof context, and carries a back-reference to that for
-  other tools that might get invoked internally (e.g.\ simplification
-  procedures \secref{sec:simproc}).  A mismatch of the context of the
-  simpset and the context of the problem being simplified may lead to
-  unexpected results.
+  For historical reasons, simpsets may occur independently from the current
+  context, but are conceptually dependent on it. When the Simplifier is
+  invoked via one of its main entry points in the Isar source language (as
+  proof method \secref{sec:simp-meth} or rule attribute
+  \secref{sec:simp-meth}), its simpset is derived from the current proof
+  context, and carries a back-reference to that for other tools that might get
+  invoked internally (e.g.\ simplification procedures \secref{sec:simproc}). A
+  mismatch of the context of the simpset and the context of the problem being
+  simplified may lead to unexpected results.
 
 
-  The implicit simpset of the theory context is propagated
-  monotonically through the theory hierarchy: forming a new theory,
-  the union of the simpsets of its imports are taken as starting
-  point.  Also note that definitional packages like @{command
-  "datatype"}, @{command "primrec"}, @{command "fun"} routinely
-  declare Simplifier rules to the target context, while plain
-  @{command "definition"} is an exception in \<^emph>\<open>not\<close> declaring
+  The implicit simpset of the theory context is propagated monotonically
+  through the theory hierarchy: forming a new theory, the union of the
+  simpsets of its imports are taken as starting point. Also note that
+  definitional packages like @{command "datatype"}, @{command "primrec"},
+  @{command "fun"} routinely declare Simplifier rules to the target context,
+  while plain @{command "definition"} is an exception in \<^emph>\<open>not\<close> declaring
   anything.
 
   \<^medskip>
-  It is up the user to manipulate the current simpset further
-  by explicitly adding or deleting theorems as simplification rules,
-  or installing other tools via simplification procedures
-  (\secref{sec:simproc}).  Good simpsets are hard to design.  Rules
-  that obviously simplify, like \<open>?n + 0 \<equiv> ?n\<close> are good
-  candidates for the implicit simpset, unless a special
-  non-normalizing behavior of certain operations is intended.  More
-  specific rules (such as distributive laws, which duplicate subterms)
-  should be added only for specific proof steps.  Conversely,
-  sometimes a rule needs to be deleted just for some part of a proof.
-  The need of frequent additions or deletions may indicate a poorly
-  designed simpset.
+  It is up the user to manipulate the current simpset further by explicitly
+  adding or deleting theorems as simplification rules, or installing other
+  tools via simplification procedures (\secref{sec:simproc}). Good simpsets
+  are hard to design. Rules that obviously simplify, like \<open>?n + 0 \<equiv> ?n\<close> are
+  good candidates for the implicit simpset, unless a special non-normalizing
+  behavior of certain operations is intended. More specific rules (such as
+  distributive laws, which duplicate subterms) should be added only for
+  specific proof steps. Conversely, sometimes a rule needs to be deleted just
+  for some part of a proof. The need of frequent additions or deletions may
+  indicate a poorly designed simpset.
 
   \begin{warn}
-  The union of simpsets from theory imports (as described above) is
-  not always a good starting point for the new theory.  If some
-  ancestors have deleted simplification rules because they are no
-  longer wanted, while others have left those rules in, then the union
-  will contain the unwanted rules, and thus have to be deleted again
-  in the theory body.
+  The union of simpsets from theory imports (as described above) is not always
+  a good starting point for the new theory. If some ancestors have deleted
+  simplification rules because they are no longer wanted, while others have
+  left those rules in, then the union will contain the unwanted rules, and
+  thus have to be deleted again in the theory body.
   \end{warn}
 \<close>
 
 
 subsection \<open>Ordered rewriting with permutative rules\<close>
 
-text \<open>A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and
-  right-hand side are the equal up to renaming of variables.  The most
-  common permutative rule is commutativity: \<open>?x + ?y = ?y +
-  ?x\<close>.  Other examples include \<open>(?x - ?y) - ?z = (?x - ?z) -
-  ?y\<close> in arithmetic and \<open>insert ?x (insert ?y ?A) = insert ?y
-  (insert ?x ?A)\<close> for sets.  Such rules are common enough to merit
-  special attention.
+text \<open>
+  A rewrite rule is \<^emph>\<open>permutative\<close> if the left-hand side and right-hand side
+  are the equal up to renaming of variables. The most common permutative rule
+  is commutativity: \<open>?x + ?y = ?y + ?x\<close>. Other examples include \<open>(?x - ?y) -
+  ?z = (?x - ?z) - ?y\<close> in arithmetic and \<open>insert ?x (insert ?y ?A) = insert ?y
+  (insert ?x ?A)\<close> for sets. Such rules are common enough to merit special
+  attention.
 
-  Because ordinary rewriting loops given such rules, the Simplifier
-  employs a special strategy, called \<^emph>\<open>ordered rewriting\<close>.
-  Permutative rules are detected and only applied if the rewriting
-  step decreases the redex wrt.\ a given term ordering.  For example,
-  commutativity rewrites \<open>b + a\<close> to \<open>a + b\<close>, but then
-  stops, because the redex cannot be decreased further in the sense of
-  the term ordering.
+  Because ordinary rewriting loops given such rules, the Simplifier employs a
+  special strategy, called \<^emph>\<open>ordered rewriting\<close>. Permutative rules are
+  detected and only applied if the rewriting step decreases the redex wrt.\ a
+  given term ordering. For example, commutativity rewrites \<open>b + a\<close> to \<open>a + b\<close>,
+  but then stops, because the redex cannot be decreased further in the sense
+  of the term ordering.
 
-  The default is lexicographic ordering of term structure, but this
-  could be also changed locally for special applications via
-  @{index_ML Simplifier.set_termless} in Isabelle/ML.
+  The default is lexicographic ordering of term structure, but this could be
+  also changed locally for special applications via @{index_ML
+  Simplifier.set_termless} in Isabelle/ML.
 
   \<^medskip>
-  Permutative rewrite rules are declared to the Simplifier
-  just like other rewrite rules.  Their special status is recognized
-  automatically, and their application is guarded by the term ordering
-  accordingly.\<close>
+  Permutative rewrite rules are declared to the Simplifier just like other
+  rewrite rules. Their special status is recognized automatically, and their
+  application is guarded by the term ordering accordingly.
+\<close>
 
 
 subsubsection \<open>Rewriting with AC operators\<close>
 
-text \<open>Ordered rewriting is particularly effective in the case of
-  associative-commutative operators.  (Associativity by itself is not
-  permutative.)  When dealing with an AC-operator \<open>f\<close>, keep
-  the following points in mind:
+text \<open>
+  Ordered rewriting is particularly effective in the case of
+  associative-commutative operators. (Associativity by itself is not
+  permutative.) When dealing with an AC-operator \<open>f\<close>, keep the following
+  points in mind:
 
-  \<^item> The associative law must always be oriented from left to
-  right, namely \<open>f (f x y) z = f x (f y z)\<close>.  The opposite
-  orientation, if used with commutativity, leads to looping in
-  conjunction with the standard term order.
+    \<^item> The associative law must always be oriented from left to right, namely
+    \<open>f (f x y) z = f x (f y z)\<close>. The opposite orientation, if used with
+    commutativity, leads to looping in conjunction with the standard term
+    order.
 
-  \<^item> To complete your set of rewrite rules, you must add not just
-  associativity (A) and commutativity (C) but also a derived rule
-  \<^emph>\<open>left-commutativity\<close> (LC): \<open>f x (f y z) = f y (f x z)\<close>.
-
+    \<^item> To complete your set of rewrite rules, you must add not just
+    associativity (A) and commutativity (C) but also a derived rule
+    \<^emph>\<open>left-commutativity\<close> (LC): \<open>f x (f y z) = f y (f x z)\<close>.
 
   Ordered rewriting with the combination of A, C, and LC sorts a term
   lexicographically --- the rewriting engine imitates bubble-sort.
@@ -704,9 +685,11 @@
 
 lemmas AC_rules = assoc commute left_commute
 
-text \<open>Thus the Simplifier is able to establish equalities with
-  arbitrary permutations of subterms, by normalizing to a common
-  standard form.  For example:\<close>
+text \<open>
+  Thus the Simplifier is able to establish equalities with arbitrary
+  permutations of subterms, by normalizing to a common standard form. For
+  example:
+\<close>
 
 lemma "(b \<bullet> c) \<bullet> a = xxx"
   apply (simp only: AC_rules)
@@ -719,10 +702,11 @@
 
 end
 
-text \<open>Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and
-  give many examples; other algebraic structures are amenable to
-  ordered rewriting, such as Boolean rings.  The Boyer-Moore theorem
-  prover @{cite bm88book} also employs ordered rewriting.
+text \<open>
+  Martin and Nipkow @{cite "martin-nipkow"} discuss the theory and give many
+  examples; other algebraic structures are amenable to ordered rewriting, such
+  as Boolean rings. The Boyer-Moore theorem prover @{cite bm88book} also
+  employs ordered rewriting.
 \<close>
 
 
@@ -761,29 +745,29 @@
   These attributes and configurations options control various aspects of
   Simplifier tracing and debugging.
 
-  \<^descr> @{attribute simp_trace} makes the Simplifier output internal
-  operations.  This includes rewrite steps, but also bookkeeping like
-  modifications of the simpset.
+  \<^descr> @{attribute simp_trace} makes the Simplifier output internal operations.
+  This includes rewrite steps, but also bookkeeping like modifications of the
+  simpset.
 
-  \<^descr> @{attribute simp_trace_depth_limit} limits the effect of
-  @{attribute simp_trace} to the given depth of recursive Simplifier
-  invocations (when solving conditions of rewrite rules).
+  \<^descr> @{attribute simp_trace_depth_limit} limits the effect of @{attribute
+  simp_trace} to the given depth of recursive Simplifier invocations (when
+  solving conditions of rewrite rules).
 
-  \<^descr> @{attribute simp_debug} makes the Simplifier output some extra
-  information about internal operations.  This includes any attempted
-  invocation of simplification procedures.
+  \<^descr> @{attribute simp_debug} makes the Simplifier output some extra information
+  about internal operations. This includes any attempted invocation of
+  simplification procedures.
 
   \<^descr> @{attribute simp_trace_new} controls Simplifier tracing within
   Isabelle/PIDE applications, notably Isabelle/jEdit @{cite "isabelle-jedit"}.
-  This provides a hierarchical representation of the rewriting steps
-  performed by the Simplifier.
+  This provides a hierarchical representation of the rewriting steps performed
+  by the Simplifier.
 
   Users can configure the behaviour by specifying breakpoints, verbosity and
   enabling or disabling the interactive mode. In normal verbosity (the
-  default), only rule applications matching a breakpoint will be shown to
-  the user. In full verbosity, all rule applications will be logged.
-  Interactive mode interrupts the normal flow of the Simplifier and defers
-  the decision how to continue to the user via some GUI dialog.
+  default), only rule applications matching a breakpoint will be shown to the
+  user. In full verbosity, all rule applications will be logged. Interactive
+  mode interrupts the normal flow of the Simplifier and defers the decision
+  how to continue to the user via some GUI dialog.
 
   \<^descr> @{attribute simp_break} declares term or theorem breakpoints for
   @{attribute simp_trace_new} as described above. Term breakpoints are
@@ -800,21 +784,19 @@
 
 subsection \<open>Simplification procedures \label{sec:simproc}\<close>
 
-text \<open>Simplification procedures are ML functions that produce proven
-  rewrite rules on demand.  They are associated with higher-order
-  patterns that approximate the left-hand sides of equations.  The
-  Simplifier first matches the current redex against one of the LHS
-  patterns; if this succeeds, the corresponding ML function is
-  invoked, passing the Simplifier context and redex term.  Thus rules
-  may be specifically fashioned for particular situations, resulting
-  in a more powerful mechanism than term rewriting by a fixed set of
-  rules.
+text \<open>
+  Simplification procedures are ML functions that produce proven rewrite rules
+  on demand. They are associated with higher-order patterns that approximate
+  the left-hand sides of equations. The Simplifier first matches the current
+  redex against one of the LHS patterns; if this succeeds, the corresponding
+  ML function is invoked, passing the Simplifier context and redex term. Thus
+  rules may be specifically fashioned for particular situations, resulting in
+  a more powerful mechanism than term rewriting by a fixed set of rules.
 
-  Any successful result needs to be a (possibly conditional) rewrite
-  rule \<open>t \<equiv> u\<close> that is applicable to the current redex.  The
-  rule will be applied just as any ordinary rewrite rule.  It is
-  expected to be already in \<^emph>\<open>internal form\<close>, bypassing the
-  automatic preprocessing of object-level equivalences.
+  Any successful result needs to be a (possibly conditional) rewrite rule \<open>t \<equiv>
+  u\<close> that is applicable to the current redex. The rule will be applied just as
+  any ordinary rewrite rule. It is expected to be already in \<^emph>\<open>internal form\<close>,
+  bypassing the automatic preprocessing of object-level equivalences.
 
   \begin{matharray}{rcl}
     @{command_def "simproc_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@@ -829,40 +811,39 @@
     @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
   \<close>}
 
-  \<^descr> @{command "simproc_setup"} defines a named simplification
-  procedure that is invoked by the Simplifier whenever any of the
-  given term patterns match the current redex.  The implementation,
-  which is provided as ML source text, needs to be of type @{ML_type
-  "morphism -> Proof.context -> cterm -> thm option"}, where the @{ML_type
-  cterm} represents the current redex \<open>r\<close> and the result is
-  supposed to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a
-  generalized version), or @{ML NONE} to indicate failure.  The
-  @{ML_type Proof.context} argument holds the full context of the current
-  Simplifier invocation.  The
-  @{ML_type morphism} informs about the difference of the original
-  compilation context wrt.\ the one of the actual application later
-  on.  The optional @{keyword "identifier"} specifies theorems that
-  represent the logical content of the abstract theory of this
-  simproc.
+  \<^descr> @{command "simproc_setup"} defines a named simplification procedure that
+  is invoked by the Simplifier whenever any of the given term patterns match
+  the current redex. The implementation, which is provided as ML source text,
+  needs to be of type
+  @{ML_type "morphism -> Proof.context -> cterm -> thm option"}, where the
+  @{ML_type cterm} represents the current redex \<open>r\<close> and the result is supposed
+  to be some proven rewrite rule \<open>r \<equiv> r'\<close> (or a generalized version), or @{ML
+  NONE} to indicate failure. The @{ML_type Proof.context} argument holds the
+  full context of the current Simplifier invocation. The @{ML_type morphism}
+  informs about the difference of the original compilation context wrt.\ the
+  one of the actual application later on. The optional @{keyword "identifier"}
+  specifies theorems that represent the logical content of the abstract theory
+  of this simproc.
 
-  Morphisms and identifiers are only relevant for simprocs that are
-  defined within a local target context, e.g.\ in a locale.
+  Morphisms and identifiers are only relevant for simprocs that are defined
+  within a local target context, e.g.\ in a locale.
 
-  \<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close>
-  add or delete named simprocs to the current Simplifier context.  The
-  default is to add a simproc.  Note that @{command "simproc_setup"}
-  already adds the new simproc to the subsequent context.
+  \<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> add or delete named simprocs
+  to the current Simplifier context. The default is to add a simproc. Note
+  that @{command "simproc_setup"} already adds the new simproc to the
+  subsequent context.
 \<close>
 
 
 subsubsection \<open>Example\<close>
 
-text \<open>The following simplification procedure for @{thm
-  [source=false, show_types] unit_eq} in HOL performs fine-grained
-  control over rule application, beyond higher-order pattern matching.
-  Declaring @{thm unit_eq} as @{attribute simp} directly would make
-  the Simplifier loop!  Note that a version of this simplification
-  procedure is already active in Isabelle/HOL.\<close>
+text \<open>
+  The following simplification procedure for @{thm [source = false,
+  show_types] unit_eq} in HOL performs fine-grained control over rule
+  application, beyond higher-order pattern matching. Declaring @{thm unit_eq}
+  as @{attribute simp} directly would make the Simplifier loop! Note that a
+  version of this simplification procedure is already active in Isabelle/HOL.
+\<close>
 
 (*<*)experiment begin(*>*)
 simproc_setup unit ("x::unit") =
@@ -871,20 +852,20 @@
     else SOME (mk_meta_eq @{thm unit_eq})\<close>
 (*<*)end(*>*)
 
-text \<open>Since the Simplifier applies simplification procedures
-  frequently, it is important to make the failure check in ML
-  reasonably fast.\<close>
+text \<open>
+  Since the Simplifier applies simplification procedures frequently, it is
+  important to make the failure check in ML reasonably fast.\<close>
 
 
 subsection \<open>Configurable Simplifier strategies \label{sec:simp-strategies}\<close>
 
-text \<open>The core term-rewriting engine of the Simplifier is normally
-  used in combination with some add-on components that modify the
-  strategy and allow to integrate other non-Simplifier proof tools.
-  These may be reconfigured in ML as explained below.  Even if the
-  default strategies of object-logics like Isabelle/HOL are used
-  unchanged, it helps to understand how the standard Simplifier
-  strategies work.\<close>
+text \<open>
+  The core term-rewriting engine of the Simplifier is normally used in
+  combination with some add-on components that modify the strategy and allow
+  to integrate other non-Simplifier proof tools. These may be reconfigured in
+  ML as explained below. Even if the default strategies of object-logics like
+  Isabelle/HOL are used unchanged, it helps to understand how the standard
+  Simplifier strategies work.\<close>
 
 
 subsubsection \<open>The subgoaler\<close>
@@ -897,21 +878,20 @@
   \end{mldecls}
 
   The subgoaler is the tactic used to solve subgoals arising out of
-  conditional rewrite rules or congruence rules.  The default should
-  be simplification itself.  In rare situations, this strategy may
-  need to be changed.  For example, if the premise of a conditional
-  rule is an instance of its conclusion, as in \<open>Suc ?m < ?n \<Longrightarrow>
-  ?m < ?n\<close>, the default strategy could loop.  % FIXME !??
+  conditional rewrite rules or congruence rules. The default should be
+  simplification itself. In rare situations, this strategy may need to be
+  changed. For example, if the premise of a conditional rule is an instance of
+  its conclusion, as in \<open>Suc ?m < ?n \<Longrightarrow> ?m < ?n\<close>, the default strategy could
+  loop. % FIXME !??
 
-  \<^descr> @{ML Simplifier.set_subgoaler}~\<open>tac ctxt\<close> sets the
-  subgoaler of the context to \<open>tac\<close>.  The tactic will
-  be applied to the context of the running Simplifier instance.
+    \<^descr> @{ML Simplifier.set_subgoaler}~\<open>tac ctxt\<close> sets the subgoaler of the
+    context to \<open>tac\<close>. The tactic will be applied to the context of the running
+    Simplifier instance.
 
-  \<^descr> @{ML Simplifier.prems_of}~\<open>ctxt\<close> retrieves the current
-  set of premises from the context.  This may be non-empty only if
-  the Simplifier has been told to utilize local assumptions in the
-  first place (cf.\ the options in \secref{sec:simp-meth}).
-
+    \<^descr> @{ML Simplifier.prems_of}~\<open>ctxt\<close> retrieves the current set of premises
+    from the context. This may be non-empty only if the Simplifier has been
+    told to utilize local assumptions in the first place (cf.\ the options in
+    \secref{sec:simp-meth}).
 
   As an example, consider the following alternative subgoaler:
 \<close>
@@ -923,9 +903,9 @@
     asm_simp_tac ctxt
 \<close>
 
-text \<open>This tactic first tries to solve the subgoal by assumption or
-  by resolving with with one of the premises, calling simplification
-  only if that fails.\<close>
+text \<open>
+  This tactic first tries to solve the subgoal by assumption or by resolving
+  with with one of the premises, calling simplification only if that fails.\<close>
 
 
 subsubsection \<open>The solver\<close>
@@ -941,89 +921,76 @@
   @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\
   \end{mldecls}
 
-  A solver is a tactic that attempts to solve a subgoal after
-  simplification.  Its core functionality is to prove trivial subgoals
-  such as @{prop "True"} and \<open>t = t\<close>, but object-logics might
-  be more ambitious.  For example, Isabelle/HOL performs a restricted
-  version of linear arithmetic here.
+  A solver is a tactic that attempts to solve a subgoal after simplification.
+  Its core functionality is to prove trivial subgoals such as @{prop "True"}
+  and \<open>t = t\<close>, but object-logics might be more ambitious. For example,
+  Isabelle/HOL performs a restricted version of linear arithmetic here.
 
-  Solvers are packaged up in abstract type @{ML_type solver}, with
-  @{ML Simplifier.mk_solver} as the only operation to create a solver.
+  Solvers are packaged up in abstract type @{ML_type solver}, with @{ML
+  Simplifier.mk_solver} as the only operation to create a solver.
 
   \<^medskip>
-  Rewriting does not instantiate unknowns.  For example,
-  rewriting alone cannot prove \<open>a \<in> ?A\<close> since this requires
-  instantiating \<open>?A\<close>.  The solver, however, is an arbitrary
-  tactic and may instantiate unknowns as it pleases.  This is the only
-  way the Simplifier can handle a conditional rewrite rule whose
-  condition contains extra variables.  When a simplification tactic is
-  to be combined with other provers, especially with the Classical
-  Reasoner, it is important whether it can be considered safe or not.
-  For this reason a simpset contains two solvers: safe and unsafe.
+  Rewriting does not instantiate unknowns. For example, rewriting alone cannot
+  prove \<open>a \<in> ?A\<close> since this requires instantiating \<open>?A\<close>. The solver, however,
+  is an arbitrary tactic and may instantiate unknowns as it pleases. This is
+  the only way the Simplifier can handle a conditional rewrite rule whose
+  condition contains extra variables. When a simplification tactic is to be
+  combined with other provers, especially with the Classical Reasoner, it is
+  important whether it can be considered safe or not. For this reason a
+  simpset contains two solvers: safe and unsafe.
 
-  The standard simplification strategy solely uses the unsafe solver,
-  which is appropriate in most cases.  For special applications where
-  the simplification process is not allowed to instantiate unknowns
-  within the goal, simplification starts with the safe solver, but may
-  still apply the ordinary unsafe one in nested simplifications for
-  conditional rules or congruences. Note that in this way the overall
-  tactic is not totally safe: it may instantiate unknowns that appear
-  also in other subgoals.
-
-  \<^descr> @{ML Simplifier.mk_solver}~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the \<open>name\<close> is only attached as a
-  comment and has no further significance.
+  The standard simplification strategy solely uses the unsafe solver, which is
+  appropriate in most cases. For special applications where the simplification
+  process is not allowed to instantiate unknowns within the goal,
+  simplification starts with the safe solver, but may still apply the ordinary
+  unsafe one in nested simplifications for conditional rules or congruences.
+  Note that in this way the overall tactic is not totally safe: it may
+  instantiate unknowns that appear also in other subgoals.
 
-  \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as
-  the safe solver of \<open>ctxt\<close>.
+  \<^descr> @{ML Simplifier.mk_solver}~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the
+  \<open>name\<close> is only attached as a comment and has no further significance.
 
-  \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an
-  additional safe solver; it will be tried after the solvers which had
-  already been present in \<open>ctxt\<close>.
+  \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the
-  unsafe solver of \<open>ctxt\<close>.
+  \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an additional safe solver; it
+  will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an
-  additional unsafe solver; it will be tried after the solvers which
-  had already been present in \<open>ctxt\<close>.
+  \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
+
+  \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an additional unsafe solver; it
+  will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
 
   \<^medskip>
-  The solver tactic is invoked with the context of the
-  running Simplifier.  Further operations
-  may be used to retrieve relevant information, such as the list of
-  local Simplifier premises via @{ML Simplifier.prems_of} --- this
-  list may be non-empty only if the Simplifier runs in a mode that
-  utilizes local assumptions (see also \secref{sec:simp-meth}).  The
-  solver is also presented the full goal including its assumptions in
-  any case.  Thus it can use these (e.g.\ by calling @{ML
-  assume_tac}), even if the Simplifier proper happens to ignore local
-  premises at the moment.
+  The solver tactic is invoked with the context of the running Simplifier.
+  Further operations may be used to retrieve relevant information, such as the
+  list of local Simplifier premises via @{ML Simplifier.prems_of} --- this
+  list may be non-empty only if the Simplifier runs in a mode that utilizes
+  local assumptions (see also \secref{sec:simp-meth}). The solver is also
+  presented the full goal including its assumptions in any case. Thus it can
+  use these (e.g.\ by calling @{ML assume_tac}), even if the Simplifier proper
+  happens to ignore local premises at the moment.
 
   \<^medskip>
-  As explained before, the subgoaler is also used to solve
-  the premises of congruence rules.  These are usually of the form
-  \<open>s = ?x\<close>, where \<open>s\<close> needs to be simplified and
-  \<open>?x\<close> needs to be instantiated with the result.  Typically,
+  As explained before, the subgoaler is also used to solve the premises of
+  congruence rules. These are usually of the form \<open>s = ?x\<close>, where \<open>s\<close> needs to
+  be simplified and \<open>?x\<close> needs to be instantiated with the result. Typically,
   the subgoaler will invoke the Simplifier at some point, which will
-  eventually call the solver.  For this reason, solver tactics must be
-  prepared to solve goals of the form \<open>t = ?x\<close>, usually by
-  reflexivity.  In particular, reflexivity should be tried before any
-  of the fancy automated proof tools.
+  eventually call the solver. For this reason, solver tactics must be prepared
+  to solve goals of the form \<open>t = ?x\<close>, usually by reflexivity. In particular,
+  reflexivity should be tried before any of the fancy automated proof tools.
 
-  It may even happen that due to simplification the subgoal is no
-  longer an equality.  For example, \<open>False \<longleftrightarrow> ?Q\<close> could be
-  rewritten to \<open>\<not> ?Q\<close>.  To cover this case, the solver could
-  try resolving with the theorem \<open>\<not> False\<close> of the
+  It may even happen that due to simplification the subgoal is no longer an
+  equality. For example, \<open>False \<longleftrightarrow> ?Q\<close> could be rewritten to \<open>\<not> ?Q\<close>. To cover
+  this case, the solver could try resolving with the theorem \<open>\<not> False\<close> of the
   object-logic.
 
   \<^medskip>
   \begin{warn}
-  If a premise of a congruence rule cannot be proved, then the
-  congruence is ignored.  This should only happen if the rule is
-  \<^emph>\<open>conditional\<close> --- that is, contains premises not of the form
-  \<open>t = ?x\<close>.  Otherwise it indicates that some congruence rule,
-  or possibly the subgoaler or solver, is faulty.
+  If a premise of a congruence rule cannot be proved, then the congruence is
+  ignored. This should only happen if the rule is \<^emph>\<open>conditional\<close> --- that is,
+  contains premises not of the form \<open>t = ?x\<close>. Otherwise it indicates that some
+  congruence rule, or possibly the subgoaler or solver, is faulty.
   \end{warn}
 \<close>
 
@@ -1042,69 +1009,62 @@
   @{index_ML Splitter.del_split: "thm -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
-  The looper is a list of tactics that are applied after
-  simplification, in case the solver failed to solve the simplified
-  goal.  If the looper succeeds, the simplification process is started
-  all over again.  Each of the subgoals generated by the looper is
-  attacked in turn, in reverse order.
+  The looper is a list of tactics that are applied after simplification, in
+  case the solver failed to solve the simplified goal. If the looper succeeds,
+  the simplification process is started all over again. Each of the subgoals
+  generated by the looper is attacked in turn, in reverse order.
 
-  A typical looper is \<^emph>\<open>case splitting\<close>: the expansion of a
-  conditional.  Another possibility is to apply an elimination rule on
-  the assumptions.  More adventurous loopers could start an induction.
+  A typical looper is \<^emph>\<open>case splitting\<close>: the expansion of a conditional.
+  Another possibility is to apply an elimination rule on the assumptions. More
+  adventurous loopers could start an induction.
 
-  \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only
-  looper tactic of \<open>ctxt\<close>.
+    \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an
-  additional looper tactic with name \<open>name\<close>, which is
-  significant for managing the collection of loopers.  The tactic will
-  be tried after the looper tactics that had already been present in
-  \<open>ctxt\<close>.
+    \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an additional looper tactic
+    with name \<open>name\<close>, which is significant for managing the collection of
+    loopers. The tactic will be tried after the looper tactics that had
+    already been present in \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was
-  associated with \<open>name\<close> from \<open>ctxt\<close>.
+    \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
+    \<open>name\<close> from \<open>ctxt\<close>.
 
-  \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactics
-  for \<open>thm\<close> as additional looper tactics of \<open>ctxt\<close>.
+    \<^descr> @{ML Splitter.add_split}~\<open>thm ctxt\<close> adds split tactics for \<open>thm\<close> as
+    additional looper tactics of \<open>ctxt\<close>.
 
-  \<^descr> @{ML Splitter.del_split}~\<open>thm ctxt\<close> deletes the split
-  tactic corresponding to \<open>thm\<close> from the looper tactics of
-  \<open>ctxt\<close>.
+    \<^descr> @{ML Splitter.del_split}~\<open>thm ctxt\<close> deletes the split tactic
+    corresponding to \<open>thm\<close> from the looper tactics of \<open>ctxt\<close>.
 
-
-  The splitter replaces applications of a given function; the
-  right-hand side of the replacement can be anything.  For example,
-  here is a splitting rule for conditional expressions:
+  The splitter replaces applications of a given function; the right-hand side
+  of the replacement can be anything. For example, here is a splitting rule
+  for conditional expressions:
 
   @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
 
-  Another example is the elimination operator for Cartesian products
-  (which happens to be called @{const case_prod} in Isabelle/HOL:
+  Another example is the elimination operator for Cartesian products (which
+  happens to be called @{const case_prod} in Isabelle/HOL:
 
   @{text [display] "?P (case_prod ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
 
-  For technical reasons, there is a distinction between case splitting
-  in the conclusion and in the premises of a subgoal.  The former is
-  done by @{ML Splitter.split_tac} with rules like @{thm [source]
-  if_split} or @{thm [source] option.split}, which do not split the
-  subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
-  with rules like @{thm [source] if_split_asm} or @{thm [source]
-  option.split_asm}, which split the subgoal.  The function @{ML
-  Splitter.add_split} automatically takes care of which tactic to
-  call, analyzing the form of the rules given as argument; it is the
-  same operation behind \<open>split\<close> attribute or method modifier
-  syntax in the Isar source language.
+  For technical reasons, there is a distinction between case splitting in the
+  conclusion and in the premises of a subgoal. The former is done by @{ML
+  Splitter.split_tac} with rules like @{thm [source] if_split} or @{thm
+  [source] option.split}, which do not split the subgoal, while the latter is
+  done by @{ML Splitter.split_asm_tac} with rules like @{thm [source]
+  if_split_asm} or @{thm [source] option.split_asm}, which split the subgoal.
+  The function @{ML Splitter.add_split} automatically takes care of which
+  tactic to call, analyzing the form of the rules given as argument; it is the
+  same operation behind \<open>split\<close> attribute or method modifier syntax in the
+  Isar source language.
 
-  Case splits should be allowed only when necessary; they are
-  expensive and hard to control.  Case-splitting on if-expressions in
-  the conclusion is usually beneficial, so it is enabled by default in
-  Isabelle/HOL and Isabelle/FOL/ZF.
+  Case splits should be allowed only when necessary; they are expensive and
+  hard to control. Case-splitting on if-expressions in the conclusion is
+  usually beneficial, so it is enabled by default in Isabelle/HOL and
+  Isabelle/FOL/ZF.
 
   \begin{warn}
-  With @{ML Splitter.split_asm_tac} as looper component, the
-  Simplifier may split subgoals!  This might cause unexpected problems
-  in tactic expressions that silently assume 0 or 1 subgoals after
-  simplification.
+  With @{ML Splitter.split_asm_tac} as looper component, the Simplifier may
+  split subgoals! This might cause unexpected problems in tactic expressions
+  that silently assume 0 or 1 subgoals after simplification.
   \end{warn}
 \<close>
 
@@ -1123,18 +1083,17 @@
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')'
   \<close>}
 
-  \<^descr> @{attribute simplified}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> causes a theorem to
-  be simplified, either by exactly the specified rules \<open>a\<^sub>1, \<dots>,
-  a\<^sub>n\<close>, or the implicit Simplifier context if no arguments are given.
-  The result is fully simplified by default, including assumptions and
-  conclusion; the options \<open>no_asm\<close> etc.\ tune the Simplifier in
-  the same way as the for the \<open>simp\<close> method.
+  \<^descr> @{attribute simplified}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> causes a theorem to be simplified,
+  either by exactly the specified rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close>, or the implicit
+  Simplifier context if no arguments are given. The result is fully simplified
+  by default, including assumptions and conclusion; the options \<open>no_asm\<close> etc.\
+  tune the Simplifier in the same way as the for the \<open>simp\<close> method.
 
-  Note that forward simplification restricts the Simplifier to its
-  most basic operation of term rewriting; solver and looper tactics
-  (\secref{sec:simp-strategies}) are \<^emph>\<open>not\<close> involved here.  The
-  @{attribute simplified} attribute should be only rarely required
-  under normal circumstances.
+  Note that forward simplification restricts the Simplifier to its most basic
+  operation of term rewriting; solver and looper tactics
+  (\secref{sec:simp-strategies}) are \<^emph>\<open>not\<close> involved here. The @{attribute
+  simplified} attribute should be only rarely required under normal
+  circumstances.
 \<close>