# HG changeset patch
# User wenzelm
# Date 1446665758 -3600
# Node ID 1ec8af91e169f72ef1f2e7802a29ed7b2247da85
# Parent  f18f6e51e901858bfa2af91c64b83d633e19ae4f
tuned whitespace;

diff -r f18f6e51e901 -r 1ec8af91e169 src/Doc/Eisbach/Manual.thy
--- a/src/Doc/Eisbach/Manual.thy	Wed Nov 04 20:18:46 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy	Wed Nov 04 20:35:58 2015 +0100
@@ -14,8 +14,8 @@
   terms, facts, or other methods.
 
   \<^medskip>
-  The syntax diagram below refers to some syntactic categories that
-  are further defined in @{cite "isabelle-isar-ref"}.
+  The syntax diagram below refers to some syntactic categories that are
+  further defined in @{cite "isabelle-isar-ref"}.
 
   @{rail \<open>
     @@{command method} name args @'=' method
@@ -56,11 +56,10 @@
       by prop_solver\<^sub>1
 
 text \<open>
-  In this example, the facts \<open>impI\<close> and \<open>conjE\<close> are static. They
-  are evaluated once when the method is defined and cannot be changed later.
-  This makes the method stable in the sense of \<^emph>\<open>static scoping\<close>: naming
-  another fact \<open>impI\<close> in a later context won't affect the behaviour of
-  \<open>prop_solver\<^sub>1\<close>.
+  In this example, the facts \<open>impI\<close> and \<open>conjE\<close> are static. They are evaluated
+  once when the method is defined and cannot be changed later. This makes the
+  method stable in the sense of \<^emph>\<open>static scoping\<close>: naming another fact \<open>impI\<close>
+  in a later context won't affect the behaviour of \<open>prop_solver\<^sub>1\<close>.
 \<close>
 
 
@@ -100,11 +99,11 @@
 subsection \<open>Named theorems\<close>
 
 text \<open>
-  A \<open>named theorem\<close> is a fact whose contents are produced dynamically
-  within the current proof context. The Isar command @{command_ref
-  "named_theorems"} provides simple access to this concept: it declares a
-  dynamic fact with corresponding \<^emph>\<open>attribute\<close> for managing
-  this particular data slot in the context.
+  A \<^emph>\<open>named theorem\<close> is a fact whose contents are produced dynamically within
+  the current proof context. The Isar command @{command_ref "named_theorems"}
+  provides simple access to this concept: it declares a dynamic fact with
+  corresponding \<^emph>\<open>attribute\<close> for managing this particular data slot in the
+  context.
 \<close>
 
     named_theorems intros
@@ -112,7 +111,8 @@
 text \<open>
   So far \<open>intros\<close> refers to the empty fact. Using the Isar command
   @{command_ref "declare"} we may apply declaration attributes to the context.
-  Below we declare both \<open>conjI\<close> and \<open>impI\<close> as \<open>intros\<close>, adding them to the named theorem slot.
+  Below we declare both \<open>conjI\<close> and \<open>impI\<close> as \<open>intros\<close>, adding them to the
+  named theorem slot.
 \<close>
 
     declare conjI [intros] and impI [intros]
@@ -136,8 +136,8 @@
 text \<open>
   Often these named theorems need to be augmented on the spot, when a method
   is invoked. The @{keyword_def "declares"} keyword in the signature of
-  @{command method} adds the common method syntax \<open>method decl: facts\<close>
-  for each named theorem \<open>decl\<close>.
+  @{command method} adds the common method syntax \<open>method decl: facts\<close> for
+  each named theorem \<open>decl\<close>.
 \<close>
 
     method prop_solver\<^sub>4 declares intros elims =
@@ -170,11 +170,12 @@
 section \<open>Higher-order methods\<close>
 
 text \<open>
-  The \<^emph>\<open>structured concatenation\<close> combinator ``\<open>method\<^sub>1 ;
-  method\<^sub>2\<close>'' was introduced in Isabelle2015, motivated by development of
-  Eisbach. It is similar to ``\<open>method\<^sub>1, method\<^sub>2\<close>'', but \<open>method\<^sub>2\<close> is invoked on on \<^emph>\<open>all\<close> subgoals that have newly emerged from
-  \<open>method\<^sub>1\<close>. This is useful to handle cases where the number of
-  subgoals produced by a method is determined dynamically at run-time.
+  The \<^emph>\<open>structured concatenation\<close> combinator ``\<open>method\<^sub>1 ; method\<^sub>2\<close>'' was
+  introduced in Isabelle2015, motivated by development of Eisbach. It is
+  similar to ``\<open>method\<^sub>1, method\<^sub>2\<close>'', but \<open>method\<^sub>2\<close> is invoked on on \<^emph>\<open>all\<close>
+  subgoals that have newly emerged from \<open>method\<^sub>1\<close>. This is useful to handle
+  cases where the number of subgoals produced by a method is determined
+  dynamically at run-time.
 \<close>
 
     method conj_with uses rule =
@@ -190,18 +191,17 @@
   method combinators with prefix syntax. For example, to more usefully exploit
   Isabelle's backtracking, the explicit requirement that a method solve all
   produced subgoals is frequently useful. This can easily be written as a
-  \<^emph>\<open>higher-order method\<close> using ``\<open>;\<close>''. The @{keyword "methods"}
-  keyword denotes method parameters that are other proof methods to be invoked
-  by the method being defined.
+  \<^emph>\<open>higher-order method\<close> using ``\<open>;\<close>''. The @{keyword "methods"} keyword
+  denotes method parameters that are other proof methods to be invoked by the
+  method being defined.
 \<close>
 
     method solve methods m = (m ; fail)
 
 text \<open>
-  Given some method-argument \<open>m\<close>, \<open>solve \<open>m\<close>\<close> applies the
-  method \<open>m\<close> and then fails whenever \<open>m\<close> produces any new unsolved
-  subgoals --- i.e. when \<open>m\<close> fails to completely discharge the goal it
-  was applied to.
+  Given some method-argument \<open>m\<close>, \<open>solve \<open>m\<close>\<close> applies the method \<open>m\<close> and then
+  fails whenever \<open>m\<close> produces any new unsolved subgoals --- i.e. when \<open>m\<close>
+  fails to completely discharge the goal it was applied to.
 \<close>
 
 
@@ -222,29 +222,31 @@
         (erule notE ; solve \<open>prop_solver\<close>))+
 
 text \<open>
-  The only non-trivial part above is the final alternative \<open>(erule notE
-  ; solve \<open>prop_solver\<close>)\<close>. Here, in the case that all other alternatives
-  fail, the method takes one of the assumptions @{term "\<not> P"} of the current
-  goal and eliminates it with the rule \<open>notE\<close>, causing the goal to be
-  proved to become @{term P}. The method then recursively invokes itself on
-  the remaining goals. The job of the recursive call is to demonstrate that
-  there is a contradiction in the original assumptions (i.e.\ that @{term P}
-  can be derived from them). Note this recursive invocation is applied with
-  the @{method solve} method combinator to ensure that a contradiction will
-  indeed be shown. In the case where a contradiction cannot be found,
-  backtracking will occur and a different assumption @{term "\<not> Q"} will be
-  chosen for elimination.
+  The only non-trivial part above is the final alternative \<open>(erule notE ;
+  solve \<open>prop_solver\<close>)\<close>. Here, in the case that all other alternatives fail,
+  the method takes one of the assumptions @{term "\<not> P"} of the current goal
+  and eliminates it with the rule \<open>notE\<close>, causing the goal to be proved to
+  become @{term P}. The method then recursively invokes itself on the
+  remaining goals. The job of the recursive call is to demonstrate that there
+  is a contradiction in the original assumptions (i.e.\ that @{term P} can be
+  derived from them). Note this recursive invocation is applied with the
+  @{method solve} method combinator to ensure that a contradiction will indeed
+  be shown. In the case where a contradiction cannot be found, backtracking
+  will occur and a different assumption @{term "\<not> Q"} will be chosen for
+  elimination.
 
   Note that the recursive call to @{method prop_solver} does not have any
-  parameters passed to it. Recall that fact parameters, e.g.\ \<open>intros\<close>, \<open>elims\<close>, and \<open>subst\<close>, are managed by declarations
-  in the current proof context. They will therefore be passed to any recursive
-  call to @{method prop_solver} and, more generally, any invocation of a
-  method which declares these named theorems.
+  parameters passed to it. Recall that fact parameters, e.g.\ \<open>intros\<close>,
+  \<open>elims\<close>, and \<open>subst\<close>, are managed by declarations in the current proof
+  context. They will therefore be passed to any recursive call to @{method
+  prop_solver} and, more generally, any invocation of a method which declares
+  these named theorems.
 
   \<^medskip>
   After declaring some standard rules to the context, the @{method
   prop_solver} becomes capable of solving non-trivial propositional
-  tautologies.\<close>
+  tautologies.
+\<close>
 
     lemmas [intros] =
       conjI  --  \<open>@{thm conjI}\<close>
@@ -271,15 +273,15 @@
   result of backtracking. When designing more sophisticated proof methods this
   proves too restrictive and difficult to manage conceptually.
 
-  To address this, we introduce the @{method_def "match"} method, which
-  provides more direct access to the higher-order matching facility at the
-  core of Isabelle. It is implemented as a separate proof method (in
-  Isabelle/ML), and thus can be directly applied to proofs, however it is most
-  useful when applied in the context of writing Eisbach method definitions.
+  To address this, we introduce the @{method_def match} method, which provides
+  more direct access to the higher-order matching facility at the core of
+  Isabelle. It is implemented as a separate proof method (in Isabelle/ML), and
+  thus can be directly applied to proofs, however it is most useful when
+  applied in the context of writing Eisbach method definitions.
 
   \<^medskip>
-  The syntax diagram below refers to some syntactic categories that
-  are further defined in @{cite "isabelle-isar-ref"}.
+  The syntax diagram below refers to some syntactic categories that are
+  further defined in @{cite "isabelle-isar-ref"}.
 
   @{rail \<open>
     @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>')
@@ -296,10 +298,10 @@
   \<close>}
 
   Matching allows methods to introspect the goal state, and to implement more
-  explicit control flow. In the basic case, a term or fact \<open>ts\<close> is given
-  to match against as a \<^emph>\<open>match target\<close>, along with a collection of
-  pattern-method pairs \<open>(p, m)\<close>: roughly speaking, when the pattern
-  \<open>p\<close> matches any member of \<open>ts\<close>, the \<^emph>\<open>inner\<close> method \<open>m\<close> will be executed.
+  explicit control flow. In the basic case, a term or fact \<open>ts\<close> is given to
+  match against as a \<^emph>\<open>match target\<close>, along with a collection of
+  pattern-method pairs \<open>(p, m)\<close>: roughly speaking, when the pattern \<open>p\<close>
+  matches any member of \<open>ts\<close>, the \<^emph>\<open>inner\<close> method \<open>m\<close> will be executed.
 \<close>
 
     lemma
@@ -310,11 +312,11 @@
         by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>)
 
 text \<open>
-  In this example we have a structured Isar proof, with the named
-  assumption \<open>X\<close> and a conclusion @{term "P"}. With the match method
-  we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to
-  separately as \<open>I\<close> and \<open>I'\<close>. We then specialize the
-  modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal.
+  In this example we have a structured Isar proof, with the named assumption
+  \<open>X\<close> and a conclusion @{term "P"}. With the match method we can find the
+  local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to separately as
+  \<open>I\<close> and \<open>I'\<close>. We then specialize the modus-ponens rule @{thm mp [of Q P]} to
+  these facts to solve the goal.
 \<close>
 
 
@@ -324,15 +326,14 @@
   In the previous example we were able to match against an assumption out of
   the Isar proof state. In general, however, proof subgoals can be
   \<^emph>\<open>unstructured\<close>, with goal parameters and premises arising from rule
-  application. To address this, @{method match} uses \<^emph>\<open>subgoal focusing\<close>
-  to produce structured goals out of
-  unstructured ones. In place of fact or term, we may give the
-  keyword @{keyword_def "premises"} as the match target. This causes a subgoal
-  focus on the first subgoal, lifting local goal parameters to fixed term
-  variables and premises into hypothetical theorems. The match is performed
-  against these theorems, naming them and binding them as appropriate.
-  Similarly giving the keyword @{keyword_def "conclusion"} matches against the
-  conclusion of the first subgoal.
+  application. To address this, @{method match} uses \<^emph>\<open>subgoal focusing\<close> to
+  produce structured goals out of unstructured ones. In place of fact or term,
+  we may give the keyword @{keyword_def "premises"} as the match target. This
+  causes a subgoal focus on the first subgoal, lifting local goal parameters
+  to fixed term variables and premises into hypothetical theorems. The match
+  is performed against these theorems, naming them and binding them as
+  appropriate. Similarly giving the keyword @{keyword_def "conclusion"}
+  matches against the conclusion of the first subgoal.
 
   An unstructured version of the previous example can then be similarly solved
   through focusing.
@@ -358,16 +359,16 @@
   now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term
   P}), finally applying the specialized rule to solve the goal.
 
-  Schematic terms like \<open>?P\<close> may also be used to specify match
-  variables, but the result of the match is not bound, and thus cannot be used
-  in the inner method body.
+  Schematic terms like \<open>?P\<close> may also be used to specify match variables, but
+  the result of the match is not bound, and thus cannot be used in the inner
+  method body.
 
   \<^medskip>
-  In the following example we extract the predicate of an
-  existentially quantified conclusion in the current subgoal and search the
-  current premises for a matching fact. If both matches are successful, we
-  then instantiate the existential introduction rule with both the witness and
-  predicate, solving with the matched premise.
+  In the following example we extract the predicate of an existentially
+  quantified conclusion in the current subgoal and search the current premises
+  for a matching fact. If both matches are successful, we then instantiate the
+  existential introduction rule with both the witness and predicate, solving
+  with the matched premise.
 \<close>
 
     method solve_ex =
@@ -378,15 +379,14 @@
 text \<open>
   The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the
   current conclusion, binding the term @{term "Q"} in the inner match. Next
-  the pattern \<open>Q y\<close> is matched against all premises of the current
-  subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be
-  instantiated. Once a match is found, the local fact \<open>U\<close> is bound to
-  the matching premise and the variable @{term "y"} is bound to the matching
-  witness. The existential introduction rule \<open>exI:\<close>~@{thm exI} is then
-  instantiated with @{term "y"} as the witness and @{term "Q"} as the
-  predicate, with its proof obligation solved by the local fact U (using the
-  Isar attribute @{attribute OF}). The following example is a trivial use of
-  this method.
+  the pattern \<open>Q y\<close> is matched against all premises of the current subgoal. In
+  this case @{term "Q"} is fixed and @{term "y"} may be instantiated. Once a
+  match is found, the local fact \<open>U\<close> is bound to the matching premise and the
+  variable @{term "y"} is bound to the matching witness. The existential
+  introduction rule \<open>exI:\<close>~@{thm exI} is then instantiated with @{term "y"} as
+  the witness and @{term "Q"} as the predicate, with its proof obligation
+  solved by the local fact U (using the Isar attribute @{attribute OF}). The
+  following example is a trivial use of this method.
 \<close>
 
     lemma "halts p \<Longrightarrow> \<exists>x. halts x"
@@ -419,13 +419,12 @@
   with a universal quantifier in the premises that matches the type of @{term
   y}. Since @{keyword "premises"} causes a focus, however, there are no
   subgoal premises to be found and thus @{method my_allE_bad} will always
-  fail. If focusing instead left the premises in place, using methods
-  like @{method erule} would lead to unintended behaviour, specifically during
+  fail. If focusing instead left the premises in place, using methods like
+  @{method erule} would lead to unintended behaviour, specifically during
   backtracking. In our example, @{method erule} could choose an alternate
-  premise while backtracking, while leaving \<open>I\<close> bound to the original
-  match. In the case of more complex inner methods, where either \<open>I\<close> or
-  bound terms are used, this would almost certainly not be the intended
-  behaviour.
+  premise while backtracking, while leaving \<open>I\<close> bound to the original match.
+  In the case of more complex inner methods, where either \<open>I\<close> or bound terms
+  are used, this would almost certainly not be the intended behaviour.
 
   An alternative implementation would be to specialize the elimination rule to
   the bound term and apply it directly.
@@ -444,13 +443,13 @@
   premise, it is not likely the intended behaviour. Repeated application of
   this method will produce an infinite stream of duplicate specialized
   premises, due to the original premise never being removed. To address this,
-  matched premises may be declared with the @{attribute "thin"} attribute.
-  This will hide the premise from subsequent inner matches, and remove it from
-  the list of premises when the inner method has finished and the subgoal is
+  matched premises may be declared with the @{attribute thin} attribute. This
+  will hide the premise from subsequent inner matches, and remove it from the
+  list of premises when the inner method has finished and the subgoal is
   unfocused. It can be considered analogous to the existing \<open>thin_tac\<close>.
 
-  To complete our example, the correct implementation of the method
-  will @{attribute "thin"} the premise from the match and then apply it to the
+  To complete our example, the correct implementation of the method will
+  @{attribute thin} the premise from the match and then apply it to the
   specialized elimination rule.\<close>
 
     method my_allE for y :: 'a =
@@ -460,13 +459,14 @@
     lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y"
       by (my_allE y)+ (rule conjI)
 
+
 subsubsection \<open>Inner focusing\<close>
 
 text \<open>
-  Premises are \<^emph>\<open>accumulated\<close> for the purposes of subgoal focusing.
-  In contrast to using standard methods like @{method frule} within
-  focused match, another @{method match} will have access to all the premises
-  of the outer focus.
+  Premises are \<^emph>\<open>accumulated\<close> for the purposes of subgoal focusing. In
+  contrast to using standard methods like @{method frule} within focused
+  match, another @{method match} will have access to all the premises of the
+  outer focus.
 \<close>
 
     lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B"
@@ -475,25 +475,23 @@
 
 text \<open>
   In this example, the inner @{method match} can find the focused premise
-  @{term B}. In contrast, the @{method assumption} method would fail here
-  due to @{term B} not being logically accessible.
+  @{term B}. In contrast, the @{method assumption} method would fail here due
+  to @{term B} not being logically accessible.
 \<close>
 
-    lemma
-    "A \<Longrightarrow> A \<and> (B \<longrightarrow> B)"
+    lemma "A \<Longrightarrow> A \<and> (B \<longrightarrow> B)"
       by (match premises in H: A \<Rightarrow> \<open>intro conjI, rule H, rule impI,
             match premises (local) in A \<Rightarrow> \<open>fail\<close>
                                  \<bar> H': B \<Rightarrow> \<open>rule H'\<close>\<close>)
 
 text \<open>
-  In this example, the only premise that exists in the first focus is
-  @{term "A"}. Prior to the inner match, the rule \<open>impI\<close> changes
-  the goal @{term "B \<longrightarrow> B"} into @{term "B \<Longrightarrow> B"}. A standard premise
-  match would also include @{term A} as an original premise of the outer
-  match. The \<open>local\<close> argument limits the match to
-  newly focused premises.
+  In this example, the only premise that exists in the first focus is @{term
+  "A"}. Prior to the inner match, the rule \<open>impI\<close> changes the goal @{term "B \<longrightarrow>
+  B"} into @{term "B \<Longrightarrow> B"}. A standard premise match would also include @{term
+  A} as an original premise of the outer match. The \<open>local\<close> argument limits
+  the match to newly focused premises.
+\<close>
 
-\<close>
 
 section \<open>Attributes\<close>
 
@@ -547,8 +545,7 @@
 text \<open>
   The @{attribute of} attribute behaves similarly. It is worth noting,
   however, that the positional instantiation of @{attribute of} occurs against
-  the position of the variables as they are declared \<^emph>\<open>in the match
-  pattern\<close>.
+  the position of the variables as they are declared \<^emph>\<open>in the match pattern\<close>.
 \<close>
 
     lemma
@@ -559,15 +556,16 @@
             \<open>rule I [of x y]\<close>)
 
 text \<open>
-  In this example, the order of schematics in \<open>asm\<close> is actually \<open>?y ?x\<close>, but we instantiate our matched rule in the opposite order. This is
-  because the effective rule @{term I} was bound from the match, which
-  declared the @{typ 'a} slot first and the @{typ 'b} slot second.
+  In this example, the order of schematics in \<open>asm\<close> is actually \<open>?y ?x\<close>, but
+  we instantiate our matched rule in the opposite order. This is because the
+  effective rule @{term I} was bound from the match, which declared the @{typ
+  'a} slot first and the @{typ 'b} slot second.
 
   To get the dynamic behaviour of @{attribute of} we can choose to invoke it
-  \<^emph>\<open>unchecked\<close>. This avoids trying to do any type inference for the
-  provided parameters, instead storing them as their most general type and
-  doing type matching at run-time. This, like @{attribute OF}, will throw
-  errors if the expected slots don't exist or there is a type mismatch.
+  \<^emph>\<open>unchecked\<close>. This avoids trying to do any type inference for the provided
+  parameters, instead storing them as their most general type and doing type
+  matching at run-time. This, like @{attribute OF}, will throw errors if the
+  expected slots don't exist or there is a type mismatch.
 \<close>
 
     lemma
@@ -587,11 +585,11 @@
             \<open>prop_solver\<close>)
 
 text \<open>
-  In this example, the pattern \<open>\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x\<close> matches against
-  the only premise, giving an appropriately typed slot for @{term y}. After
-  the match, the resulting rule is instantiated to @{term y} and then declared
-  as an @{attribute intros} rule. This is then picked up by @{method
-  prop_solver} to solve the goal.
+  In this example, the pattern \<open>\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x\<close> matches against the
+  only premise, giving an appropriately typed slot for @{term y}. After the
+  match, the resulting rule is instantiated to @{term y} and then declared as
+  an @{attribute intros} rule. This is then picked up by @{method prop_solver}
+  to solve the goal.
 \<close>
 
 
@@ -600,8 +598,9 @@
 text \<open>
   In all previous examples, @{method match} was only ever searching for a
   single rule or premise. Each local fact would therefore always have a length
-  of exactly one. We may, however, wish to find \<^emph>\<open>all\<close> matching results.
-  To achieve this, we can simply mark a given pattern with the \<open>(multi)\<close> argument.
+  of exactly one. We may, however, wish to find \<^emph>\<open>all\<close> matching results. To
+  achieve this, we can simply mark a given pattern with the \<open>(multi)\<close>
+  argument.
 \<close>
 
     lemma
@@ -612,21 +611,21 @@
       done
 
 text \<open>
-  In the first @{method match}, without the \<open>(multi)\<close> argument, @{term
-  I} is only ever be bound to one of the members of \<open>asms\<close>. This
-  backtracks over both possibilities (see next section), however neither
-  assumption in isolation is sufficient to solve to goal. The use of the
-  @{method solves} combinator ensures that @{method prop_solver} has no effect
-  on the goal when it doesn't solve it, and so the first match leaves the goal
-  unchanged. In the second @{method match}, \<open>I\<close> is bound to all of
-  \<open>asms\<close>, declaring both results as \<open>intros\<close>. With these rules
-  @{method prop_solver} is capable of solving the goal.
+  In the first @{method match}, without the \<open>(multi)\<close> argument, @{term I} is
+  only ever be bound to one of the members of \<open>asms\<close>. This backtracks over
+  both possibilities (see next section), however neither assumption in
+  isolation is sufficient to solve to goal. The use of the @{method solves}
+  combinator ensures that @{method prop_solver} has no effect on the goal when
+  it doesn't solve it, and so the first match leaves the goal unchanged. In
+  the second @{method match}, \<open>I\<close> is bound to all of \<open>asms\<close>, declaring both
+  results as \<open>intros\<close>. With these rules @{method prop_solver} is capable of
+  solving the goal.
 
   Using for-fixed variables in patterns imposes additional constraints on the
-  results. In all previous examples, the choice of using \<open>?P\<close> or a
-  for-fixed @{term P} only depended on whether or not @{term P} was mentioned
-  in another pattern or the inner method. When using a multi-match, however,
-  all for-fixed terms must agree in the results.
+  results. In all previous examples, the choice of using \<open>?P\<close> or a for-fixed
+  @{term P} only depended on whether or not @{term P} was mentioned in another
+  pattern or the inner method. When using a multi-match, however, all
+  for-fixed terms must agree in the results.
 \<close>
 
     lemma
@@ -641,11 +640,11 @@
 text \<open>
   Here we have two seemingly-equivalent applications of @{method match},
   however only the second one is capable of solving the goal. The first
-  @{method match} selects the first and third members of \<open>asms\<close> (those
-  that agree on their conclusion), which is not sufficient. The second
-  @{method match} selects the first and second members of \<open>asms\<close> (those
-  that agree on their assumption), which is enough for @{method prop_solver}
-  to solve the goal.
+  @{method match} selects the first and third members of \<open>asms\<close> (those that
+  agree on their conclusion), which is not sufficient. The second @{method
+  match} selects the first and second members of \<open>asms\<close> (those that agree on
+  their assumption), which is enough for @{method prop_solver} to solve the
+  goal.
 \<close>
 
 
@@ -655,10 +654,10 @@
   Dummy patterns may be given as placeholders for unique schematics in
   patterns. They implicitly receive all currently bound variables as
   arguments, and are coerced into the @{typ prop} type whenever possible. For
-  example, the trivial dummy pattern \<open>_\<close> will match any proposition.
-  In contrast, by default the pattern \<open>?P\<close> is considered to have type
-  @{typ bool}. It will not bind anything with meta-logical connectives (e.g.
-  \<open>_ \<Longrightarrow> _\<close> or \<open>_ &&& _\<close>).
+  example, the trivial dummy pattern \<open>_\<close> will match any proposition. In
+  contrast, by default the pattern \<open>?P\<close> is considered to have type @{typ
+  bool}. It will not bind anything with meta-logical connectives (e.g. \<open>_ \<Longrightarrow> _\<close>
+  or \<open>_ &&& _\<close>).
 \<close>
 
     lemma
@@ -670,19 +669,19 @@
 section \<open>Backtracking\<close>
 
 text \<open>
-  Patterns are considered top-down, executing the inner method \<open>m\<close> of
-  the first pattern which is satisfied by the current match target. By
-  default, matching performs extensive backtracking by attempting all valid
-  variable and fact bindings according to the given pattern. In particular,
-  all unifiers for a given pattern will be explored, as well as each matching
+  Patterns are considered top-down, executing the inner method \<open>m\<close> of the
+  first pattern which is satisfied by the current match target. By default,
+  matching performs extensive backtracking by attempting all valid variable
+  and fact bindings according to the given pattern. In particular, all
+  unifiers for a given pattern will be explored, as well as each matching
   fact. The inner method \<open>m\<close> will be re-executed for each different
   variable/fact binding during backtracking. A successful match is considered
   a cut-point for backtracking. Specifically, once a match is made no other
   pattern-method pairs will be considered.
 
-  The method \<open>foo\<close> below fails for all goals that are conjunctions. Any
-  such goal will match the first pattern, causing the second pattern (that
-  would otherwise match all goals) to never be considered.
+  The method \<open>foo\<close> below fails for all goals that are conjunctions. Any such
+  goal will match the first pattern, causing the second pattern (that would
+  otherwise match all goals) to never be considered.
 \<close>
 
     method foo =
@@ -690,12 +689,12 @@
 
 text \<open>
   The failure of an inner method that is executed after a successful match
-  will cause the entire match to fail. This distinction is important
-  due to the pervasive use of backtracking. When a method is used in a
-  combinator chain, its failure
-  becomes significant because it signals previously applied methods to move to
-  the next result. Therefore, it is necessary for @{method match} to not mask
-  such failure. One can always rewrite a match using the combinators ``\<open>?\<close>'' and ``\<open>|\<close>'' to try subsequent patterns in the case of an
+  will cause the entire match to fail. This distinction is important due to
+  the pervasive use of backtracking. When a method is used in a combinator
+  chain, its failure becomes significant because it signals previously applied
+  methods to move to the next result. Therefore, it is necessary for @{method
+  match} to not mask such failure. One can always rewrite a match using the
+  combinators ``\<open>?\<close>'' and ``\<open>|\<close>'' to try subsequent patterns in the case of an
   inner-method failure. The following proof method, for example, always
   invokes @{method prop_solver} for all goals because its first alternative
   either never matches or (if it does match) always fails.
@@ -710,8 +709,8 @@
 
 text \<open>
   Backtracking may be controlled more precisely by marking individual patterns
-  as \<open>cut\<close>. This causes backtracking to not progress beyond this pattern:
-  once a match is found no others will be considered.
+  as \<open>cut\<close>. This causes backtracking to not progress beyond this pattern: once
+  a match is found no others will be considered.
 \<close>
 
     method foo\<^sub>2 =
@@ -722,10 +721,10 @@
   In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible
   implications of @{term "P"} in the premises are considered, evaluating the
   inner @{method rule} with each consequent. No other conjunctions will be
-  considered, with method failure occurring once all implications of the
-  form \<open>P \<longrightarrow> ?U\<close> have been explored. Here the left-right processing of
-  individual patterns is important, as all patterns after of the cut will
-  maintain their usual backtracking behaviour.
+  considered, with method failure occurring once all implications of the form
+  \<open>P \<longrightarrow> ?U\<close> have been explored. Here the left-right processing of individual
+  patterns is important, as all patterns after of the cut will maintain their
+  usual backtracking behaviour.
 \<close>
 
     lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
@@ -735,16 +734,16 @@
       by (foo\<^sub>2 | prop_solver)
 
 text \<open>
-  In this example, the first lemma is solved by \<open>foo\<^sub>2\<close>, by first
-  picking @{term "A \<longrightarrow> D"} for \<open>I'\<close>, then backtracking and ultimately
-  succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however,
-  @{term "C \<and> D"} is matched first, the second pattern in the match cannot be
-  found and so the method fails, falling through to @{method prop_solver}.
+  In this example, the first lemma is solved by \<open>foo\<^sub>2\<close>, by first picking
+  @{term "A \<longrightarrow> D"} for \<open>I'\<close>, then backtracking and ultimately succeeding after
+  picking @{term "A \<longrightarrow> C"}. In the second lemma, however, @{term "C \<and> D"} is
+  matched first, the second pattern in the match cannot be found and so the
+  method fails, falling through to @{method prop_solver}.
 
-  More precise control is also possible by giving a positive
-  number \<open>n\<close> as an argument to \<open>cut\<close>. This will limit the number
-  of backtracking results of that match to be at most \<open>n\<close>.
-  The match argument \<open>(cut 1)\<close> is the same as simply \<open>(cut)\<close>.
+  More precise control is also possible by giving a positive number \<open>n\<close> as an
+  argument to \<open>cut\<close>. This will limit the number of backtracking results of
+  that match to be at most \<open>n\<close>. The match argument \<open>(cut 1)\<close> is the same as
+  simply \<open>(cut)\<close>.
 \<close>
 
 
@@ -769,15 +768,16 @@
 
 text \<open>
   Intuitively it seems like this proof should fail to check. The first match
-  result, which binds @{term I} to the first two members of \<open>asms\<close>,
-  fails the second inner match due to binding @{term P} to @{term A}.
-  Backtracking then attempts to bind @{term I} to the third member of \<open>asms\<close>. This passes all inner matches, but fails when @{method rule} cannot
-  successfully apply this to the current goal. After this, a valid match that
-  is produced by the unifier is one which binds @{term P} to simply \<open>\<lambda>a. A ?x\<close>. The first inner match succeeds because \<open>\<lambda>a. A ?x\<close> does
-  not match @{term A}. The next inner match succeeds because @{term I} has
-  only been bound to the first member of \<open>asms\<close>. This is due to @{method
-  match} considering \<open>\<lambda>a. A ?x\<close> and \<open>\<lambda>a. A ?y\<close> as distinct
-  terms.
+  result, which binds @{term I} to the first two members of \<open>asms\<close>, fails the
+  second inner match due to binding @{term P} to @{term A}. Backtracking then
+  attempts to bind @{term I} to the third member of \<open>asms\<close>. This passes all
+  inner matches, but fails when @{method rule} cannot successfully apply this
+  to the current goal. After this, a valid match that is produced by the
+  unifier is one which binds @{term P} to simply \<open>\<lambda>a. A ?x\<close>. The first inner
+  match succeeds because \<open>\<lambda>a. A ?x\<close> does not match @{term A}. The next inner
+  match succeeds because @{term I} has only been bound to the first member of
+  \<open>asms\<close>. This is due to @{method match} considering \<open>\<lambda>a. A ?x\<close> and \<open>\<lambda>a. A ?y\<close>
+  as distinct terms.
 
   The simplest way to address this is to explicitly disallow term bindings
   which we would consider invalid.
@@ -797,8 +797,8 @@
 text \<open>
   The @{method match} method is not aware of the logical content of match
   targets. Each pattern is simply matched against the shallow structure of a
-  fact or term. Most facts are in \<^emph>\<open>normal form\<close>, which curries premises
-  via meta-implication \<open>_ \<Longrightarrow> _\<close>.
+  fact or term. Most facts are in \<^emph>\<open>normal form\<close>, which curries premises via
+  meta-implication \<open>_ \<Longrightarrow> _\<close>.
 \<close>
 
     lemma
@@ -821,17 +821,17 @@
 text \<open>
   This proof will fail to solve the goal. Our match pattern will only match
   rules which have a single premise, and conclusion @{term C}, so the first
-  member of \<open>asms\<close> is not bound and thus the proof fails. Matching a
-  pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"}
-  to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a
-  concrete @{term "C"} in the conclusion, will fail to match this fact.
+  member of \<open>asms\<close> is not bound and thus the proof fails. Matching a pattern
+  of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"} to
+  @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a concrete
+  @{term "C"} in the conclusion, will fail to match this fact.
 
-  To express our desired match, we may \<^emph>\<open>uncurry\<close> our rules before
-  matching against them. This forms a meta-conjunction of all premises in a
-  fact, so that only one implication remains. For example the uncurried
-  version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match
-  our desired pattern \<open>_ \<Longrightarrow> C\<close>, and can be \<^emph>\<open>curried\<close> after the
-  match to put it back into normal form.
+  To express our desired match, we may \<^emph>\<open>uncurry\<close> our rules before matching
+  against them. This forms a meta-conjunction of all premises in a fact, so
+  that only one implication remains. For example the uncurried version of
+  @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match our
+  desired pattern \<open>_ \<Longrightarrow> C\<close>, and can be \<^emph>\<open>curried\<close> after the match to put it
+  back into normal form.
 \<close>
 
     lemma
@@ -858,12 +858,12 @@
       done
 
 text \<open>
-  In the first @{method match} we attempt to find a member of \<open>asms\<close>
-  which matches our goal precisely. This fails due to no such member existing.
-  The second match reverses the role of the fact in the match, by first giving
-  a general pattern @{term P}. This bound pattern is then matched against
-  @{term "A y"}. In this case, @{term P} is bound to \<open>A ?x\<close> and so it
-  successfully matches.
+  In the first @{method match} we attempt to find a member of \<open>asms\<close> which
+  matches our goal precisely. This fails due to no such member existing. The
+  second match reverses the role of the fact in the match, by first giving a
+  general pattern @{term P}. This bound pattern is then matched against @{term
+  "A y"}. In this case, @{term P} is bound to \<open>A ?x\<close> and so it successfully
+  matches.
 \<close>
 
 
@@ -883,9 +883,10 @@
           \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H [where z = y]\<close>\<close>)
 
 text \<open>
-  In this example the type \<open>'b\<close> is matched to \<open>'a\<close>, however
-  statically they are formally distinct types. The first match binds \<open>'b\<close> while the inner match serves to coerce @{term y} into having the type
-  \<open>'b\<close>. This allows the rule instantiation to successfully apply.
+  In this example the type \<open>'b\<close> is matched to \<open>'a\<close>, however statically they
+  are formally distinct types. The first match binds \<open>'b\<close> while the inner
+  match serves to coerce @{term y} into having the type \<open>'b\<close>. This allows the
+  rule instantiation to successfully apply.
 \<close>
 
 
@@ -922,10 +923,10 @@
 
 text \<open>
   A custom rule attribute is a simple way to extend the functionality of
-  Eisbach methods. The dummy rule attribute notation (\<open>[[ _ ]]\<close>)
-  invokes the given attribute against a dummy fact and evaluates to the result
-  of that attribute. When used as a match target, this can serve as an
-  effective auxiliary function.
+  Eisbach methods. The dummy rule attribute notation (\<open>[[ _ ]]\<close>) invokes the
+  given attribute against a dummy fact and evaluates to the result of that
+  attribute. When used as a match target, this can serve as an effective
+  auxiliary function.
 \<close>
 
     attribute_setup get_split_rule =
diff -r f18f6e51e901 -r 1ec8af91e169 src/Doc/Eisbach/Preface.thy
--- a/src/Doc/Eisbach/Preface.thy	Wed Nov 04 20:18:46 2015 +0100
+++ b/src/Doc/Eisbach/Preface.thy	Wed Nov 04 20:35:58 2015 +0100
@@ -5,10 +5,10 @@
 begin
 
 text \<open>
-  \<^emph>\<open>Eisbach\<close> is a collection of tools which form the basis for defining
-  new proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought
-  of as a ``proof method language'', but is more precisely an infrastructure
-  for defining new proof methods out of existing ones.
+  \<^emph>\<open>Eisbach\<close> is a collection of tools which form the basis for defining new
+  proof methods in Isabelle/Isar~@{cite "Wenzel-PhD"}. It can be thought of as
+  a ``proof method language'', but is more precisely an infrastructure for
+  defining new proof methods out of existing ones.
 
   The core functionality of Eisbach is provided by the Isar @{command method}
   command. Here users may define new methods by combining existing ones with
@@ -27,8 +27,8 @@
   high barrier-to-entry for many users.
 
   \<^medskip>
-  This manual is written for users familiar with Isabelle/Isar, but
-  not necessarily Isabelle/ML. It covers the usage of the @{command method} as
+  This manual is written for users familiar with Isabelle/Isar, but not
+  necessarily Isabelle/ML. It covers the usage of the @{command method} as
   well as the @{method match} method, as well as discussing their integration
   with existing Isar concepts such as @{command named_theorems}.
 \<close>