# HG changeset patch
# User wenzelm
# Date 1447423618 -3600
# Node ID 5b878bc6ae98259c9ec235ab68cdba201a6f0f17
# Parent  cfabbc0839777547c103a99fa9ff658b6111e67b
tuned whitespace;

diff -r cfabbc083977 -r 5b878bc6ae98 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 14:49:30 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Fri Nov 13 15:06:58 2015 +0100
@@ -7,38 +7,33 @@
 chapter \<open>Proofs \label{ch:proofs}\<close>
 
 text \<open>
-
-  Proof commands perform transitions of Isar/VM machine
-  configurations, which are block-structured, consisting of a stack of
-  nodes with three main components: logical proof context, current
-  facts, and open goals.  Isar/VM transitions are typed according to
-  the following three different modes of operation:
-
-  \<^descr> \<open>proof(prove)\<close> means that a new goal has just been
-  stated that is now to be \<^emph>\<open>proven\<close>; the next command may refine
-  it by some proof method, and enter a sub-proof to establish the
-  actual result.
-
-  \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the
-  context may be augmented by \<^emph>\<open>stating\<close> additional assumptions,
-  intermediate results etc.
+  Proof commands perform transitions of Isar/VM machine configurations, which
+  are block-structured, consisting of a stack of nodes with three main
+  components: logical proof context, current facts, and open goals. Isar/VM
+  transitions are typed according to the following three different modes of
+  operation:
 
-  \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and \<open>proof(prove)\<close>: existing facts (i.e.\ the
-  contents of the special @{fact_ref this} register) have been just picked
-  up in order to be used when refining the goal claimed next.
-
+    \<^descr> \<open>proof(prove)\<close> means that a new goal has just been stated that is now to
+    be \<^emph>\<open>proven\<close>; the next command may refine it by some proof method, and
+    enter a sub-proof to establish the actual result.
+  
+    \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the context may be
+    augmented by \<^emph>\<open>stating\<close> additional assumptions, intermediate results etc.
+  
+    \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and
+    \<open>proof(prove)\<close>: existing facts (i.e.\ the contents of the special
+    @{fact_ref this} register) have been just picked up in order to be used
+    when refining the goal claimed next.
 
-  The proof mode indicator may be understood as an instruction to the
-  writer, telling what kind of operation may be performed next.  The
-  corresponding typings of proof commands restricts the shape of
-  well-formed proof texts to particular command sequences.  So dynamic
-  arrangements of commands eventually turn out as static texts of a
-  certain structure.
+  The proof mode indicator may be understood as an instruction to the writer,
+  telling what kind of operation may be performed next. The corresponding
+  typings of proof commands restricts the shape of well-formed proof texts to
+  particular command sequences. So dynamic arrangements of commands eventually
+  turn out as static texts of a certain structure.
 
-  \Appref{ap:refcard} gives a simplified grammar of the (extensible)
-  language emerging that way from the different types of proof
-  commands.  The main ideas of the overall Isar framework are
-  explained in \chref{ch:isar-framework}.
+  \Appref{ap:refcard} gives a simplified grammar of the (extensible) language
+  emerging that way from the different types of proof commands. The main ideas
+  of the overall Isar framework are explained in \chref{ch:isar-framework}.
 \<close>
 
 
@@ -57,9 +52,9 @@
     @@{command end}
   \<close>}
 
-  \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without
-  any goal statement. This allows to experiment with Isar, without producing
-  any persistent result. The notepad is closed by @{command "end"}.
+  \<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without any
+  goal statement. This allows to experiment with Isar, without producing any
+  persistent result. The notepad is closed by @{command "end"}.
 \<close>
 
 
@@ -72,32 +67,30 @@
     @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   \end{matharray}
 
-  While Isar is inherently block-structured, opening and closing
-  blocks is mostly handled rather casually, with little explicit
-  user-intervention.  Any local goal statement automatically opens
-  \<^emph>\<open>two\<close> internal blocks, which are closed again when concluding
-  the sub-proof (by @{command "qed"} etc.).  Sections of different
-  context within a sub-proof may be switched via @{command "next"},
-  which is just a single block-close followed by block-open again.
-  The effect of @{command "next"} is to reset the local proof context;
+  While Isar is inherently block-structured, opening and closing blocks is
+  mostly handled rather casually, with little explicit user-intervention. Any
+  local goal statement automatically opens \<^emph>\<open>two\<close> internal blocks, which are
+  closed again when concluding the sub-proof (by @{command "qed"} etc.).
+  Sections of different context within a sub-proof may be switched via
+  @{command "next"}, which is just a single block-close followed by block-open
+  again. The effect of @{command "next"} is to reset the local proof context;
   there is no goal focus involved here!
 
   For slightly more advanced applications, there are explicit block
-  parentheses as well.  These typically achieve a stronger forward
-  style of reasoning.
+  parentheses as well. These typically achieve a stronger forward style of
+  reasoning.
 
-  \<^descr> @{command "next"} switches to a fresh block within a
-  sub-proof, resetting the local context to the initial one.
+  \<^descr> @{command "next"} switches to a fresh block within a sub-proof, resetting
+  the local context to the initial one.
 
-  \<^descr> @{command "{"} and @{command "}"} explicitly open and close
-  blocks.  Any current facts pass through ``@{command "{"}''
-  unchanged, while ``@{command "}"}'' causes any result to be
-  \<^emph>\<open>exported\<close> into the enclosing context.  Thus fixed variables
-  are generalized, assumptions discharged, and local definitions
-  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
-  of @{command "assume"} and @{command "presume"} in this mode of
-  forward reasoning --- in contrast to plain backward reasoning with
-  the result exported at @{command "show"} time.
+  \<^descr> @{command "{"} and @{command "}"} explicitly open and close blocks. Any
+  current facts pass through ``@{command "{"}'' unchanged, while ``@{command
+  "}"}'' causes any result to be \<^emph>\<open>exported\<close> into the enclosing context. Thus
+  fixed variables are generalized, assumptions discharged, and local
+  definitions unfolded (cf.\ \secref{sec:proof-context}). There is no
+  difference of @{command "assume"} and @{command "presume"} in this mode of
+  forward reasoning --- in contrast to plain backward reasoning with the
+  result exported at @{command "show"} time.
 \<close>
 
 
@@ -108,23 +101,20 @@
     @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\
   \end{matharray}
 
-  The @{command "oops"} command discontinues the current proof
-  attempt, while considering the partial proof text as properly
-  processed.  This is conceptually quite different from ``faking''
-  actual proofs via @{command_ref "sorry"} (see
-  \secref{sec:proof-steps}): @{command "oops"} does not observe the
-  proof structure at all, but goes back right to the theory level.
-  Furthermore, @{command "oops"} does not produce any result theorem
-  --- there is no intended claim to be able to complete the proof
-  in any way.
+  The @{command "oops"} command discontinues the current proof attempt, while
+  considering the partial proof text as properly processed. This is
+  conceptually quite different from ``faking'' actual proofs via @{command_ref
+  "sorry"} (see \secref{sec:proof-steps}): @{command "oops"} does not observe
+  the proof structure at all, but goes back right to the theory level.
+  Furthermore, @{command "oops"} does not produce any result theorem --- there
+  is no intended claim to be able to complete the proof in any way.
 
   A typical application of @{command "oops"} is to explain Isar proofs
-  \<^emph>\<open>within\<close> the system itself, in conjunction with the document
-  preparation tools of Isabelle described in \chref{ch:document-prep}.
-  Thus partial or even wrong proof attempts can be discussed in a
-  logically sound manner.  Note that the Isabelle {\LaTeX} macros can
-  be easily adapted to print something like ``\<open>\<dots>\<close>'' instead of
-  the keyword ``@{command "oops"}''.
+  \<^emph>\<open>within\<close> the system itself, in conjunction with the document preparation
+  tools of Isabelle described in \chref{ch:document-prep}. Thus partial or
+  even wrong proof attempts can be discussed in a logically sound manner. Note
+  that the Isabelle {\LaTeX} macros can be easily adapted to print something
+  like ``\<open>\<dots>\<close>'' instead of the keyword ``@{command "oops"}''.
 \<close>
 
 
@@ -140,34 +130,31 @@
     @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
   \end{matharray}
 
-  The logical proof context consists of fixed variables and
-  assumptions.  The former closely correspond to Skolem constants, or
-  meta-level universal quantification as provided by the Isabelle/Pure
-  logical framework.  Introducing some \<^emph>\<open>arbitrary, but fixed\<close>
-  variable via ``@{command "fix"}~\<open>x\<close>'' results in a local value
-  that may be used in the subsequent proof as any other variable or
-  constant.  Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close> exported from
-  the context will be universally closed wrt.\ \<open>x\<close> at the
-  outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal
-  form using Isabelle's meta-variables).
+  The logical proof context consists of fixed variables and assumptions. The
+  former closely correspond to Skolem constants, or meta-level universal
+  quantification as provided by the Isabelle/Pure logical framework.
+  Introducing some \<^emph>\<open>arbitrary, but fixed\<close> variable via ``@{command
+  "fix"}~\<open>x\<close>'' results in a local value that may be used in the subsequent
+  proof as any other variable or constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close>
+  exported from the context will be universally closed wrt.\ \<open>x\<close> at the
+  outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal form using
+  Isabelle's meta-variables).
 
-  Similarly, introducing some assumption \<open>\<chi>\<close> has two effects.
-  On the one hand, a local theorem is created that may be used as a
-  fact in subsequent proof steps.  On the other hand, any result
-  \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context becomes conditional wrt.\
-  the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>.  Thus, solving an enclosing goal
-  using such a result would basically introduce a new subgoal stemming
-  from the assumption.  How this situation is handled depends on the
-  version of assumption command used: while @{command "assume"}
-  insists on solving the subgoal by unification with some premise of
-  the goal, @{command "presume"} leaves the subgoal unchanged in order
-  to be proved later by the user.
+  Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. On the one hand,
+  a local theorem is created that may be used as a fact in subsequent proof
+  steps. On the other hand, any result \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context
+  becomes conditional wrt.\ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an
+  enclosing goal using such a result would basically introduce a new subgoal
+  stemming from the assumption. How this situation is handled depends on the
+  version of assumption command used: while @{command "assume"} insists on
+  solving the subgoal by unification with some premise of the goal, @{command
+  "presume"} leaves the subgoal unchanged in order to be proved later by the
+  user.
 
-  Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv>
-  t\<close>'', are achieved by combining ``@{command "fix"}~\<open>x\<close>'' with
-  another version of assumption that causes any hypothetical equation
-  \<open>x \<equiv> t\<close> to be eliminated by the reflexivity rule.  Thus,
-  exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
+  Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv> t\<close>'', are achieved
+  by combining ``@{command "fix"}~\<open>x\<close>'' with another version of assumption
+  that causes any hypothetical equation \<open>x \<equiv> t\<close> to be eliminated by the
+  reflexivity rule. Thus, exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
   \<phi>[t]\<close>.
 
   @{rail \<open>
@@ -181,27 +168,27 @@
       @{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
   \<close>}
 
-  \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, but fixed\<close>.
+  \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary,
+  but fixed\<close>.
 
-  \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command
-  "presume"}~\<open>a: \<phi>\<close> introduce a local fact \<open>\<phi> \<turnstile> \<phi>\<close> by
-  assumption.  Subsequent results applied to an enclosing goal (e.g.\
-  by @{command_ref "show"}) are handled as follows: @{command
-  "assume"} expects to be able to unify with existing premises in the
-  goal, while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
+  \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command "presume"}~\<open>a: \<phi>\<close> introduce a
+  local fact \<open>\<phi> \<turnstile> \<phi>\<close> by assumption. Subsequent results applied to an enclosing
+  goal (e.g.\ by @{command_ref "show"}) are handled as follows: @{command
+  "assume"} expects to be able to unify with existing premises in the goal,
+  while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
 
-  Several lists of assumptions may be given (separated by
-  @{keyword_ref "and"}; the resulting list of current facts consists
-  of all of these concatenated.
+  Several lists of assumptions may be given (separated by @{keyword_ref
+  "and"}; the resulting list of current facts consists of all of these
+  concatenated.
 
-  \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local
-  (non-polymorphic) definition.  In results exported from the context,
-  \<open>x\<close> is replaced by \<open>t\<close>.  Basically, ``@{command
-  "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>x \<equiv> t\<close>'', with the resulting
-  hypothetical equation solved by reflexivity.
+  \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
+  In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
+  ``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command
+  "assume"}~\<open>x \<equiv> t\<close>'', with the resulting hypothetical equation solved by
+  reflexivity.
 
-  The default name for the definitional equation is \<open>x_def\<close>.
-  Several simultaneous definitions may be given at the same time.
+  The default name for the definitional equation is \<open>x_def\<close>. Several
+  simultaneous definitions may be given at the same time.
 \<close>
 
 
@@ -213,31 +200,28 @@
     @{keyword_def "is"} & : & syntax \\
   \end{matharray}
 
-  Abbreviations may be either bound by explicit @{command
-  "let"}~\<open>p \<equiv> t\<close> statements, or by annotating assumptions or
-  goal statements with a list of patterns ``\<open>(\<IS> p\<^sub>1 \<dots>
-  p\<^sub>n)\<close>''.  In both cases, higher-order matching is invoked to
-  bind extra-logical term variables, which may be either named
-  schematic variables of the form \<open>?x\<close>, or nameless dummies
-  ``@{variable _}'' (underscore). Note that in the @{command "let"}
-  form the patterns occur on the left-hand side, while the @{keyword
-  "is"} patterns are in postfix position.
+  Abbreviations may be either bound by explicit @{command "let"}~\<open>p \<equiv> t\<close>
+  statements, or by annotating assumptions or goal statements with a list of
+  patterns ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''. In both cases, higher-order matching is
+  invoked to bind extra-logical term variables, which may be either named
+  schematic variables of the form \<open>?x\<close>, or nameless dummies ``@{variable _}''
+  (underscore). Note that in the @{command "let"} form the patterns occur on
+  the left-hand side, while the @{keyword "is"} patterns are in postfix
+  position.
 
-  Polymorphism of term bindings is handled in Hindley-Milner style,
-  similar to ML.  Type variables referring to local assumptions or
-  open goal statements are \<^emph>\<open>fixed\<close>, while those of finished
-  results or bound by @{command "let"} may occur in \<^emph>\<open>arbitrary\<close>
-  instances later.  Even though actual polymorphism should be rarely
-  used in practice, this mechanism is essential to achieve proper
-  incremental type-inference, as the user proceeds to build up the
-  Isar proof text from left to right.
+  Polymorphism of term bindings is handled in Hindley-Milner style, similar to
+  ML. Type variables referring to local assumptions or open goal statements
+  are \<^emph>\<open>fixed\<close>, while those of finished results or bound by @{command "let"}
+  may occur in \<^emph>\<open>arbitrary\<close> instances later. Even though actual polymorphism
+  should be rarely used in practice, this mechanism is essential to achieve
+  proper incremental type-inference, as the user proceeds to build up the Isar
+  proof text from left to right.
 
   \<^medskip>
-  Term abbreviations are quite different from local
-  definitions as introduced via @{command "def"} (see
-  \secref{sec:proof-context}).  The latter are visible within the
-  logic as actual equations, while abbreviations disappear during the
-  input process just after type checking.  Also note that @{command
+  Term abbreviations are quite different from local definitions as introduced
+  via @{command "def"} (see \secref{sec:proof-context}). The latter are
+  visible within the logic as actual equations, while abbreviations disappear
+  during the input process just after type checking. Also note that @{command
   "def"} does not support polymorphism.
 
   @{rail \<open>
@@ -247,26 +231,24 @@
   The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
   @{syntax prop_pat} (see \secref{sec:term-decls}).
 
-  \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any
-  text variables in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous
-  higher-order matching against terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
+    \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any text variables
+    in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous higher-order matching against
+    terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
 
-  \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but
-  matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> against the preceding statement.  Also
-  note that @{keyword "is"} is not a separate command, but part of
-  others (such as @{command "assume"}, @{command "have"} etc.).
-
+    \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but matches \<open>p\<^sub>1, \<dots>,
+    p\<^sub>n\<close> against the preceding statement. Also note that @{keyword "is"} is
+    not a separate command, but part of others (such as @{command "assume"},
+    @{command "have"} etc.).
 
-  Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations}
-  for goals and facts are available as well.  For any open goal,
-  @{variable_ref thesis} refers to its object-level statement,
-  abstracted over any meta-level parameters (if present).  Likewise,
-  @{variable_ref this} is bound for fact statements resulting from
-  assumptions or finished goals.  In case @{variable this} refers to
-  an object-logic statement that is an application \<open>f t\<close>, then
-  \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}''
-  (three dots).  The canonical application of this convenience are
-  calculational proofs (see \secref{sec:calculation}).
+  Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} for goals and
+  facts are available as well. For any open goal, @{variable_ref thesis}
+  refers to its object-level statement, abstracted over any meta-level
+  parameters (if present). Likewise, @{variable_ref this} is bound for fact
+  statements resulting from assumptions or finished goals. In case @{variable
+  this} refers to an object-logic statement that is an application \<open>f t\<close>, then
+  \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}'' (three dots).
+  The canonical application of this convenience are calculational proofs (see
+  \secref{sec:calculation}).
 \<close>
 
 
@@ -282,16 +264,15 @@
     @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
   \end{matharray}
 
-  New facts are established either by assumption or proof of local
-  statements.  Any fact will usually be involved in further proofs,
-  either as explicit arguments of proof methods, or when forward
-  chaining towards the next goal via @{command "then"} (and variants);
-  @{command "from"} and @{command "with"} are composite forms
-  involving @{command "note"}.  The @{command "using"} elements
-  augments the collection of used facts \<^emph>\<open>after\<close> a goal has been
-  stated.  Note that the special theorem name @{fact_ref this} refers
-  to the most recently established facts, but only \<^emph>\<open>before\<close>
-  issuing a follow-up claim.
+  New facts are established either by assumption or proof of local statements.
+  Any fact will usually be involved in further proofs, either as explicit
+  arguments of proof methods, or when forward chaining towards the next goal
+  via @{command "then"} (and variants); @{command "from"} and @{command
+  "with"} are composite forms involving @{command "note"}. The @{command
+  "using"} elements augments the collection of used facts \<^emph>\<open>after\<close> a goal has
+  been stated. Note that the special theorem name @{fact_ref this} refers to
+  the most recently established facts, but only \<^emph>\<open>before\<close> issuing a follow-up
+  claim.
 
   @{rail \<open>
     @@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
@@ -300,55 +281,51 @@
       (@{syntax thmrefs} + @'and')
   \<close>}
 
-  \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts
-  \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>, binding the result as \<open>a\<close>.  Note that
-  attributes may be involved as well, both on the left and right hand
-  sides.
+  \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>,
+  binding the result as \<open>a\<close>. Note that attributes may be involved as well,
+  both on the left and right hand sides.
 
-  \<^descr> @{command "then"} indicates forward chaining by the current
-  facts in order to establish the goal to be claimed next.  The
-  initial proof method invoked to refine that will be offered the
-  facts to do ``anything appropriate'' (see also
-  \secref{sec:proof-steps}).  For example, method @{method (Pure) rule}
-  (see \secref{sec:pure-meth-att}) would typically do an elimination
-  rather than an introduction.  Automatic methods usually insert the
-  facts into the goal state before operation.  This provides a simple
-  scheme to control relevance of facts in automated proof search.
+  \<^descr> @{command "then"} indicates forward chaining by the current facts in order
+  to establish the goal to be claimed next. The initial proof method invoked
+  to refine that will be offered the facts to do ``anything appropriate'' (see
+  also \secref{sec:proof-steps}). For example, method @{method (Pure) rule}
+  (see \secref{sec:pure-meth-att}) would typically do an elimination rather
+  than an introduction. Automatic methods usually insert the facts into the
+  goal state before operation. This provides a simple scheme to control
+  relevance of facts in automated proof search.
 
-  \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command
-  "note"}~\<open>b\<close>~@{command "then"}''; thus @{command "then"} is
-  equivalent to ``@{command "from"}~\<open>this\<close>''.
+  \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command "note"}~\<open>b\<close>~@{command
+  "then"}''; thus @{command "then"} is equivalent to ``@{command
+  "from"}~\<open>this\<close>''.
 
-  \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command
-  "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n \<AND> this\<close>''; thus the forward chaining
-  is from earlier facts together with the current ones.
+  \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n
+  \<AND> this\<close>''; thus the forward chaining is from earlier facts together
+  with the current ones.
 
-  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being
-  currently indicated for use by a subsequent refinement step (such as
-  @{command_ref "apply"} or @{command_ref "proof"}).
+  \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being currently
+  indicated for use by a subsequent refinement step (such as @{command_ref
+  "apply"} or @{command_ref "proof"}).
 
-  \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally
-  similar to @{command "using"}, but unfolds definitional equations
-  \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the goal state and facts.
+  \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally similar to @{command
+  "using"}, but unfolds definitional equations \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the
+  goal state and facts.
 
 
-  Forward chaining with an empty list of theorems is the same as not
-  chaining at all.  Thus ``@{command "from"}~\<open>nothing\<close>'' has no
-  effect apart from entering \<open>prove(chain)\<close> mode, since
-  @{fact_ref nothing} is bound to the empty list of theorems.
+  Forward chaining with an empty list of theorems is the same as not chaining
+  at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no effect apart from
+  entering \<open>prove(chain)\<close> mode, since @{fact_ref nothing} is bound to the
+  empty list of theorems.
 
   Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
-  facts to be given in their proper order, corresponding to a prefix
-  of the premises of the rule involved.  Note that positions may be
-  easily skipped using something like @{command "from"}~\<open>_
-  \<AND> a \<AND> b\<close>, for example.  This involves the trivial rule
-  \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in Isabelle/Pure as
-  ``@{fact_ref "_"}'' (underscore).
+  facts to be given in their proper order, corresponding to a prefix of the
+  premises of the rule involved. Note that positions may be easily skipped
+  using something like @{command "from"}~\<open>_ \<AND> a \<AND> b\<close>, for example.
+  This involves the trivial rule \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in
+  Isabelle/Pure as ``@{fact_ref "_"}'' (underscore).
 
-  Automated methods (such as @{method simp} or @{method auto}) just
-  insert any given facts before their usual operation.  Depending on
-  the kind of procedure involved, the order of facts is less
-  significant here.
+  Automated methods (such as @{method simp} or @{method auto}) just insert any
+  given facts before their usual operation. Depending on the kind of procedure
+  involved, the order of facts is less significant here.
 \<close>
 
 
@@ -368,34 +345,31 @@
     @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
   \end{matharray}
 
-  From a theory context, proof mode is entered by an initial goal command
-  such as @{command "lemma"}. Within a proof context, new claims may be
-  introduced locally; there are variants to interact with the overall proof
-  structure specifically, such as @{command have} or @{command show}.
+  From a theory context, proof mode is entered by an initial goal command such
+  as @{command "lemma"}. Within a proof context, new claims may be introduced
+  locally; there are variants to interact with the overall proof structure
+  specifically, such as @{command have} or @{command show}.
 
-  Goals may consist of multiple statements, resulting in a list of
-  facts eventually.  A pending multi-goal is internally represented as
-  a meta-level conjunction (\<open>&&&\<close>), which is usually
-  split into the corresponding number of sub-goals prior to an initial
-  method application, via @{command_ref "proof"}
+  Goals may consist of multiple statements, resulting in a list of facts
+  eventually. A pending multi-goal is internally represented as a meta-level
+  conjunction (\<open>&&&\<close>), which is usually split into the corresponding number of
+  sub-goals prior to an initial method application, via @{command_ref "proof"}
   (\secref{sec:proof-steps}) or @{command_ref "apply"}
-  (\secref{sec:tactic-commands}).  The @{method_ref induct} method
-  covered in \secref{sec:cases-induct} acts on multiple claims
-  simultaneously.
+  (\secref{sec:tactic-commands}). The @{method_ref induct} method covered in
+  \secref{sec:cases-induct} acts on multiple claims simultaneously.
 
-  Claims at the theory level may be either in short or long form.  A
-  short goal merely consists of several simultaneous propositions
-  (often just one).  A long goal includes an explicit context
-  specification for the subsequent conclusion, involving local
-  parameters and assumptions.  Here the role of each part of the
-  statement is explicitly marked by separate keywords (see also
-  \secref{sec:locale}); the local assumptions being introduced here
-  are available as @{fact_ref assms} in the proof.  Moreover, there
-  are two kinds of conclusions: @{element_def "shows"} states several
-  simultaneous propositions (essentially a big conjunction), while
-  @{element_def "obtains"} claims several simultaneous simultaneous
-  contexts of (essentially a big disjunction of eliminated parameters
-  and assumptions, cf.\ \secref{sec:obtain}).
+  Claims at the theory level may be either in short or long form. A short goal
+  merely consists of several simultaneous propositions (often just one). A
+  long goal includes an explicit context specification for the subsequent
+  conclusion, involving local parameters and assumptions. Here the role of
+  each part of the statement is explicitly marked by separate keywords (see
+  also \secref{sec:locale}); the local assumptions being introduced here are
+  available as @{fact_ref assms} in the proof. Moreover, there are two kinds
+  of conclusions: @{element_def "shows"} states several simultaneous
+  propositions (essentially a big conjunction), while @{element_def "obtains"}
+  claims several simultaneous simultaneous contexts of (essentially a big
+  disjunction of eliminated parameters and assumptions, cf.\
+  \secref{sec:obtain}).
 
   @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@ -422,70 +396,64 @@
       (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
-  \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with
-  \<open>\<phi>\<close> as main goal, eventually resulting in some fact \<open>\<turnstile>
-  \<phi>\<close> to be put back into the target context.  An additional @{syntax
-  context} specification may build up an initial proof context for the
-  subsequent claim; this includes local definitions and syntax as
-  well, see also @{syntax "includes"} in \secref{sec:bundle} and
-  @{syntax context_elem} in \secref{sec:locale}.
+  \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with \<open>\<phi>\<close> as main goal,
+  eventually resulting in some fact \<open>\<turnstile> \<phi>\<close> to be put back into the target
+  context. An additional @{syntax context} specification may build up an
+  initial proof context for the subsequent claim; this includes local
+  definitions and syntax as well, see also @{syntax "includes"} in
+  \secref{sec:bundle} and @{syntax context_elem} in \secref{sec:locale}.
 
-  \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command
-  "proposition"} are the same as @{command "lemma"}. The different command
-  names merely serve as a formal comment in the theory source.
+  \<^descr> @{command "theorem"}, @{command "corollary"}, and @{command "proposition"}
+  are the same as @{command "lemma"}. The different command names merely serve
+  as a formal comment in the theory source.
 
-  \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"},
-  but allows the statement to contain unbound schematic variables.
+  \<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, but allows
+  the statement to contain unbound schematic variables.
 
-  Under normal circumstances, an Isar proof text needs to specify
-  claims explicitly.  Schematic goals are more like goals in Prolog,
-  where certain results are synthesized in the course of reasoning.
-  With schematic statements, the inherent compositionality of Isar
-  proofs is lost, which also impacts performance, because proof
-  checking is forced into sequential mode.
+  Under normal circumstances, an Isar proof text needs to specify claims
+  explicitly. Schematic goals are more like goals in Prolog, where certain
+  results are synthesized in the course of reasoning. With schematic
+  statements, the inherent compositionality of Isar proofs is lost, which also
+  impacts performance, because proof checking is forced into sequential mode.
 
-  \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal,
-  eventually resulting in a fact within the current logical context.
-  This operation is completely independent of any pending sub-goals of
-  an enclosing goal statements, so @{command "have"} may be freely
-  used for experimental exploration of potential results within a
-  proof body.
+  \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, eventually resulting in a
+  fact within the current logical context. This operation is completely
+  independent of any pending sub-goals of an enclosing goal statements, so
+  @{command "have"} may be freely used for experimental exploration of
+  potential results within a proof body.
 
-  \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command
-  "have"}~\<open>a: \<phi>\<close> plus a second stage to refine some pending
-  sub-goal for each one of the finished result, after having been
-  exported into the corresponding context (at the head of the
-  sub-proof of this @{command "show"} command).
+  \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command "have"}~\<open>a: \<phi>\<close> plus a second
+  stage to refine some pending sub-goal for each one of the finished result,
+  after having been exported into the corresponding context (at the head of
+  the sub-proof of this @{command "show"} command).
 
-  To accommodate interactive debugging, resulting rules are printed
-  before being applied internally.  Even more, interactive execution
-  of @{command "show"} predicts potential failure and displays the
-  resulting error as a warning beforehand.  Watch out for the
-  following message:
+  To accommodate interactive debugging, resulting rules are printed before
+  being applied internally. Even more, interactive execution of @{command
+  "show"} predicts potential failure and displays the resulting error as a
+  warning beforehand. Watch out for the following message:
   @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
 
-  \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command
-  "have"}'', i.e.\ claims a local goal to be proven by forward
-  chaining the current facts.  Note that @{command "hence"} is also
-  equivalent to ``@{command "from"}~\<open>this\<close>~@{command "have"}''.
+  \<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command "have"}'',
+  i.e.\ claims a local goal to be proven by forward chaining the current
+  facts. Note that @{command "hence"} is also equivalent to ``@{command
+  "from"}~\<open>this\<close>~@{command "have"}''.
 
-  \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command
-  "show"}''.  Note that @{command "thus"} is also equivalent to
-  ``@{command "from"}~\<open>this\<close>~@{command "show"}''.
+  \<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command "show"}''.
+  Note that @{command "thus"} is also equivalent to ``@{command
+  "from"}~\<open>this\<close>~@{command "show"}''.
 
-  \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the
-  current theory or proof context in long statement form, according to
-  the syntax for @{command "lemma"} given above.
+  \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the current theory or
+  proof context in long statement form, according to the syntax for @{command
+  "lemma"} given above.
 
 
-  Any goal statement causes some term abbreviations (such as
-  @{variable_ref "?thesis"}) to be bound automatically, see also
-  \secref{sec:term-abbrev}.
+  Any goal statement causes some term abbreviations (such as @{variable_ref
+  "?thesis"}) to be bound automatically, see also \secref{sec:term-abbrev}.
 
   Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref
   "when"} define the special fact @{fact_ref that} to refer to these
-  assumptions in the proof body. The user may provide separate names
-  according to the syntax of the statement.
+  assumptions in the proof body. The user may provide separate names according
+  to the syntax of the statement.
 \<close>
 
 
@@ -503,38 +471,34 @@
     @{attribute symmetric} & : & \<open>attribute\<close> \\
   \end{matharray}
 
-  Calculational proof is forward reasoning with implicit application
-  of transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>,
-  \<open><\<close>).  Isabelle/Isar maintains an auxiliary fact register
-  @{fact_ref calculation} for accumulating results obtained by
-  transitivity composed with the current result.  Command @{command
-  "also"} updates @{fact calculation} involving @{fact this}, while
-  @{command "finally"} exhibits the final @{fact calculation} by
-  forward chaining towards the next goal statement.  Both commands
-  require valid current facts, i.e.\ may occur only after commands
-  that produce theorems such as @{command "assume"}, @{command
-  "note"}, or some finished proof of @{command "have"}, @{command
-  "show"} etc.  The @{command "moreover"} and @{command "ultimately"}
-  commands are similar to @{command "also"} and @{command "finally"},
-  but only collect further results in @{fact calculation} without
-  applying any rules yet.
+  Calculational proof is forward reasoning with implicit application of
+  transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, \<open><\<close>). Isabelle/Isar maintains an
+  auxiliary fact register @{fact_ref calculation} for accumulating results
+  obtained by transitivity composed with the current result. Command @{command
+  "also"} updates @{fact calculation} involving @{fact this}, while @{command
+  "finally"} exhibits the final @{fact calculation} by forward chaining
+  towards the next goal statement. Both commands require valid current facts,
+  i.e.\ may occur only after commands that produce theorems such as @{command
+  "assume"}, @{command "note"}, or some finished proof of @{command "have"},
+  @{command "show"} etc. The @{command "moreover"} and @{command "ultimately"}
+  commands are similar to @{command "also"} and @{command "finally"}, but only
+  collect further results in @{fact calculation} without applying any rules
+  yet.
 
-  Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has
-  its canonical application with calculational proofs.  It refers to
-  the argument of the preceding statement. (The argument of a curried
-  infix expression happens to be its right-hand side.)
+  Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has its canonical
+  application with calculational proofs. It refers to the argument of the
+  preceding statement. (The argument of a curried infix expression happens to
+  be its right-hand side.)
 
-  Isabelle/Isar calculations are implicitly subject to block structure
-  in the sense that new threads of calculational reasoning are
-  commenced for any new block (as opened by a local goal, for
-  example).  This means that, apart from being able to nest
-  calculations, there is no separate \<^emph>\<open>begin-calculation\<close> command
-  required.
+  Isabelle/Isar calculations are implicitly subject to block structure in the
+  sense that new threads of calculational reasoning are commenced for any new
+  block (as opened by a local goal, for example). This means that, apart from
+  being able to nest calculations, there is no separate \<^emph>\<open>begin-calculation\<close>
+  command required.
 
   \<^medskip>
-  The Isar calculation proof commands may be defined as
-  follows:\<^footnote>\<open>We suppress internal bookkeeping such as proper
-  handling of block-structure.\<close>
+  The Isar calculation proof commands may be defined as follows:\<^footnote>\<open>We suppress
+  internal bookkeeping such as proper handling of block-structure.\<close>
 
   \begin{matharray}{rcl}
     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
@@ -550,49 +514,46 @@
     @@{attribute trans} (() | 'add' | 'del')
   \<close>}
 
-  \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary
-  @{fact calculation} register as follows.  The first occurrence of
-  @{command "also"} in some calculational thread initializes @{fact
-  calculation} by @{fact this}. Any subsequent @{command "also"} on
-  the same level of block-structure updates @{fact calculation} by
-  some transitivity rule applied to @{fact calculation} and @{fact
-  this} (in that order).  Transitivity rules are picked from the
-  current context, unless alternative rules are given as explicit
+  \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary @{fact
+  calculation} register as follows. The first occurrence of @{command "also"}
+  in some calculational thread initializes @{fact calculation} by @{fact
+  this}. Any subsequent @{command "also"} on the same level of block-structure
+  updates @{fact calculation} by some transitivity rule applied to @{fact
+  calculation} and @{fact this} (in that order). Transitivity rules are picked
+  from the current context, unless alternative rules are given as explicit
   arguments.
 
-  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact
-  calculation} in the same way as @{command "also"}, and concludes the
-  current calculational thread.  The final result is exhibited as fact
-  for forward chaining towards the next goal. Basically, @{command
-  "finally"} just abbreviates @{command "also"}~@{command
-  "from"}~@{fact calculation}.  Typical idioms for concluding
+  \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact calculation} in the
+  same way as @{command "also"}, and concludes the current calculational
+  thread. The final result is exhibited as fact for forward chaining towards
+  the next goal. Basically, @{command "finally"} just abbreviates @{command
+  "also"}~@{command "from"}~@{fact calculation}. Typical idioms for concluding
   calculational proofs are ``@{command "finally"}~@{command
-  "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command
-  "finally"}~@{command "have"}~\<open>\<phi>\<close>~@{command "."}''.
+  "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command "finally"}~@{command
+  "have"}~\<open>\<phi>\<close>~@{command "."}''.
 
-  \<^descr> @{command "moreover"} and @{command "ultimately"} are
-  analogous to @{command "also"} and @{command "finally"}, but collect
-  results only, without applying rules.
+  \<^descr> @{command "moreover"} and @{command "ultimately"} are analogous to
+  @{command "also"} and @{command "finally"}, but collect results only,
+  without applying rules.
 
-  \<^descr> @{command "print_trans_rules"} prints the list of transitivity
-  rules (for calculational commands @{command "also"} and @{command
-  "finally"}) and symmetry rules (for the @{attribute symmetric}
-  operation and single step elimination patters) of the current
-  context.
+  \<^descr> @{command "print_trans_rules"} prints the list of transitivity rules (for
+  calculational commands @{command "also"} and @{command "finally"}) and
+  symmetry rules (for the @{attribute symmetric} operation and single step
+  elimination patters) of the current context.
 
   \<^descr> @{attribute trans} declares theorems as transitivity rules.
 
-  \<^descr> @{attribute sym} declares symmetry rules, as well as
-  @{attribute "Pure.elim"}\<open>?\<close> rules.
+  \<^descr> @{attribute sym} declares symmetry rules, as well as @{attribute
+  "Pure.elim"}\<open>?\<close> rules.
 
-  \<^descr> @{attribute symmetric} resolves a theorem with some rule
-  declared as @{attribute sym} in the current context.  For example,
-  ``@{command "assume"}~\<open>[symmetric]: x = y\<close>'' produces a
-  swapped fact derived from that assumption.
+  \<^descr> @{attribute symmetric} resolves a theorem with some rule declared as
+  @{attribute sym} in the current context. For example, ``@{command
+  "assume"}~\<open>[symmetric]: x = y\<close>'' produces a swapped fact derived from that
+  assumption.
 
-  In structured proof texts it is often more appropriate to use an
-  explicit single-step elimination proof, such as ``@{command
-  "assume"}~\<open>x = y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
+  In structured proof texts it is often more appropriate to use an explicit
+  single-step elimination proof, such as ``@{command "assume"}~\<open>x =
+  y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
 \<close>
 
 
@@ -600,16 +561,16 @@
 
 subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
 
-text \<open>Proof methods are either basic ones, or expressions composed of
-  methods via ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural
-  composition), ``\<^verbatim>\<open>|\<close>'' (alternative
-  choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
-  once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first
-  \<open>n\<close> subgoals). In practice, proof methods are usually just a comma
-  separated list of @{syntax nameref}~@{syntax args} specifications. Note
-  that parentheses may be dropped for single method specifications (with no
-  arguments). The syntactic precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close>
-  \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low to high).
+text \<open>
+  Proof methods are either basic ones, or expressions composed of methods via
+  ``\<^verbatim>\<open>,\<close>'' (sequential composition), ``\<^verbatim>\<open>;\<close>'' (structural composition),
+  ``\<^verbatim>\<open>|\<close>'' (alternative choices), ``\<^verbatim>\<open>?\<close>'' (try), ``\<^verbatim>\<open>+\<close>'' (repeat at least
+  once), ``\<^verbatim>\<open>[\<close>\<open>n\<close>\<^verbatim>\<open>]\<close>'' (restriction to first \<open>n\<close> subgoals). In practice,
+  proof methods are usually just a comma separated list of @{syntax
+  nameref}~@{syntax args} specifications. Note that parentheses may be dropped
+  for single method specifications (with no arguments). The syntactic
+  precedence of method combinators is \<^verbatim>\<open>|\<close> \<^verbatim>\<open>;\<close> \<^verbatim>\<open>,\<close> \<^verbatim>\<open>[]\<close> \<^verbatim>\<open>+\<close> \<^verbatim>\<open>?\<close> (from low
+  to high).
 
   @{rail \<open>
     @{syntax_def method}:
@@ -618,35 +579,34 @@
     methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|')
   \<close>}
 
-  Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but
-  refer to the first subgoal or to all subgoals uniformly. Nonetheless,
-  the subsequent mechanisms allow to imitate the effect of subgoal
-  addressing that is known from ML tactics.
+  Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but refer
+  to the first subgoal or to all subgoals uniformly. Nonetheless, the
+  subsequent mechanisms allow to imitate the effect of subgoal addressing that
+  is known from ML tactics.
 
   \<^medskip>
-  Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a
-  way that certain subgoals are exposed, and other subgoals are ``parked''
-  elsewhere. Thus a proof method has no other chance than to operate on the
-  subgoals that are presently exposed.
+  Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a way that
+  certain subgoals are exposed, and other subgoals are ``parked'' elsewhere.
+  Thus a proof method has no other chance than to operate on the subgoals that
+  are presently exposed.
 
-  Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means
-  that method \<open>m\<^sub>1\<close> is applied with restriction to the first subgoal,
-  then \<open>m\<^sub>2\<close> is applied consecutively with restriction to each subgoal
-  that has newly emerged due to \<open>m\<^sub>1\<close>. This is analogous to the tactic
-  combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
-  "isabelle-implementation"}. For example, \<open>(rule r; blast)\<close> applies
-  rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
+  Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is
+  applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
+  consecutively with restriction to each subgoal that has newly emerged due to
+  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator @{ML_op THEN_ALL_NEW} in
+  Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
+  r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
 
-  Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes
-  only the first \<open>n\<close> subgoals (which need to exist), with default
-  \<open>n = 1\<close>. For example, the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals, while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
+  Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes only the
+  first \<open>n\<close> subgoals (which need to exist), with default \<open>n = 1\<close>. For example,
+  the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals,
+  while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
   applying rule \<open>r\<close> to the originally first one.
 
   \<^medskip>
-  Improper methods, notably tactic emulations, offer low-level goal
-  addressing as explicit argument to the individual tactic being involved.
-  Here ``\<open>[!]\<close>'' refers to all goals, and ``\<open>[n-]\<close>'' to all
-  goals starting from \<open>n\<close>.
+  Improper methods, notably tactic emulations, offer low-level goal addressing
+  as explicit argument to the individual tactic being involved. Here ``\<open>[!]\<close>''
+  refers to all goals, and ``\<open>[n-]\<close>'' to all goals starting from \<open>n\<close>.
 
   @{rail \<open>
     @{syntax_def goal_spec}:
@@ -668,39 +628,37 @@
     @{method_def standard} & : & \<open>method\<close> \\
   \end{matharray}
 
-  Arbitrary goal refinement via tactics is considered harmful.
-  Structured proof composition in Isar admits proof methods to be
-  invoked in two places only.
-
-  \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref
-  "proof"}~\<open>m\<^sub>1\<close> reduces a newly stated goal to a number
-  of sub-goals that are to be solved later.  Facts are passed to
-  \<open>m\<^sub>1\<close> for forward chaining, if so indicated by \<open>proof(chain)\<close> mode.
+  Arbitrary goal refinement via tactics is considered harmful. Structured
+  proof composition in Isar admits proof methods to be invoked in two places
+  only.
 
-  \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to solve remaining goals.  No facts are
-  passed to \<open>m\<^sub>2\<close>.
-
+    \<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref "proof"}~\<open>m\<^sub>1\<close> reduces a
+    newly stated goal to a number of sub-goals that are to be solved later.
+    Facts are passed to \<open>m\<^sub>1\<close> for forward chaining, if so indicated by
+    \<open>proof(chain)\<close> mode.
+  
+    \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to
+    solve remaining goals. No facts are passed to \<open>m\<^sub>2\<close>.
 
-  The only other (proper) way to affect pending goals in a proof body
-  is by @{command_ref "show"}, which involves an explicit statement of
-  what is to be solved eventually.  Thus we avoid the fundamental
-  problem of unstructured tactic scripts that consist of numerous
-  consecutive goal transformations, with invisible effects.
+  The only other (proper) way to affect pending goals in a proof body is by
+  @{command_ref "show"}, which involves an explicit statement of what is to be
+  solved eventually. Thus we avoid the fundamental problem of unstructured
+  tactic scripts that consist of numerous consecutive goal transformations,
+  with invisible effects.
 
   \<^medskip>
-  As a general rule of thumb for good proof style, initial
-  proof methods should either solve the goal completely, or constitute
-  some well-understood reduction to new sub-goals.  Arbitrary
-  automatic proof tools that are prone leave a large number of badly
-  structured sub-goals are no help in continuing the proof document in
-  an intelligible manner.
+  As a general rule of thumb for good proof style, initial proof methods
+  should either solve the goal completely, or constitute some well-understood
+  reduction to new sub-goals. Arbitrary automatic proof tools that are prone
+  leave a large number of badly structured sub-goals are no help in continuing
+  the proof document in an intelligible manner.
 
-  Unless given explicitly by the user, the default initial method is
-  @{method standard}, which subsumes at least @{method_ref (Pure) rule} or
-  its classical variant @{method_ref (HOL) rule}. These methods apply a
-  single standard elimination or introduction rule according to the topmost
-  logical connective involved. There is no separate default terminal method.
-  Any remaining goals are always solved by assumption in the very last step.
+  Unless given explicitly by the user, the default initial method is @{method
+  standard}, which subsumes at least @{method_ref (Pure) rule} or its
+  classical variant @{method_ref (HOL) rule}. These methods apply a single
+  standard elimination or introduction rule according to the topmost logical
+  connective involved. There is no separate default terminal method. Any
+  remaining goals are always solved by assumption in the very last step.
 
   @{rail \<open>
     @@{command proof} method?
@@ -712,70 +670,64 @@
     (@@{command "."} | @@{command ".."} | @@{command sorry})
   \<close>}
 
-  \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof
-  method \<open>m\<^sub>1\<close>; facts for forward chaining are passed if so
-  indicated by \<open>proof(chain)\<close> mode.
+  \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof method \<open>m\<^sub>1\<close>; facts for
+  forward chaining are passed if so indicated by \<open>proof(chain)\<close> mode.
 
-  \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by
-  proof method \<open>m\<^sub>2\<close> and concludes the sub-proof by assumption.
-  If the goal had been \<open>show\<close> (or \<open>thus\<close>), some
-  pending sub-goal is solved as well by the rule resulting from the
-  result \<^emph>\<open>exported\<close> into the enclosing goal context.  Thus \<open>qed\<close> may fail for two reasons: either \<open>m\<^sub>2\<close> fails, or the
-  resulting rule does not fit to any pending goal\<^footnote>\<open>This
-  includes any additional ``strong'' assumptions as introduced by
-  @{command "assume"}.\<close> of the enclosing context.  Debugging such a
-  situation might involve temporarily changing @{command "show"} into
-  @{command "have"}, or weakening the local context by replacing
-  occurrences of @{command "assume"} by @{command "presume"}.
+  \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by proof method \<open>m\<^sub>2\<close>
+  and concludes the sub-proof by assumption. If the goal had been \<open>show\<close> (or
+  \<open>thus\<close>), some pending sub-goal is solved as well by the rule resulting from
+  the result \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail
+  for two reasons: either \<open>m\<^sub>2\<close> fails, or the resulting rule does not fit to
+  any pending goal\<^footnote>\<open>This includes any additional ``strong'' assumptions as
+  introduced by @{command "assume"}.\<close> of the enclosing context. Debugging such
+  a situation might involve temporarily changing @{command "show"} into
+  @{command "have"}, or weakening the local context by replacing occurrences
+  of @{command "assume"} by @{command "presume"}.
 
-  \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal
-  proof\<close>\index{proof!terminal}; it abbreviates @{command
-  "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
-  backtracking across both methods.  Debugging an unsuccessful
-  @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its
-  definition; in many cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even
-  \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient to see the
-  problem.
+  \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal proof\<close>\index{proof!terminal}; it
+  abbreviates @{command "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
+  backtracking across both methods. Debugging an unsuccessful @{command
+  "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its definition; in many
+  cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient
+  to see the problem.
 
-  \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard
-  proof\<close>\index{proof!standard}; it abbreviates @{command "by"}~\<open>standard\<close>.
+  \<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard proof\<close>\index{proof!standard}; it
+  abbreviates @{command "by"}~\<open>standard\<close>.
 
-  \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial
-  proof\<close>\index{proof!trivial}; it abbreviates @{command "by"}~\<open>this\<close>.
+  \<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial proof\<close>\index{proof!trivial}; it
+  abbreviates @{command "by"}~\<open>this\<close>.
 
-  \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake}
-  pretending to solve the pending claim without further ado.  This
-  only works in interactive development, or if the @{attribute
-  quick_and_dirty} is enabled.  Facts emerging from fake
-  proofs are not the real thing.  Internally, the derivation object is
-  tainted by an oracle invocation, which may be inspected via the
+  \<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} pretending to
+  solve the pending claim without further ado. This only works in interactive
+  development, or if the @{attribute quick_and_dirty} is enabled. Facts
+  emerging from fake proofs are not the real thing. Internally, the derivation
+  object is tainted by an oracle invocation, which may be inspected via the
   theorem status @{cite "isabelle-implementation"}.
 
   The most important application of @{command "sorry"} is to support
   experimentation and top-down proof development.
 
-  \<^descr> @{method standard} refers to the default refinement step of some
-  Isar language elements (notably @{command proof} and ``@{command ".."}'').
-  It is \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the
-  application environment.
+  \<^descr> @{method standard} refers to the default refinement step of some Isar
+  language elements (notably @{command proof} and ``@{command ".."}''). It is
+  \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the application
+  environment.
 
   In Isabelle/Pure, @{method standard} performs elementary introduction~/
-  elimination steps (@{method_ref (Pure) rule}), introduction of type
-  classes (@{method_ref intro_classes}) and locales (@{method_ref
-  intro_locales}).
+  elimination steps (@{method_ref (Pure) rule}), introduction of type classes
+  (@{method_ref intro_classes}) and locales (@{method_ref intro_locales}).
 
-  In Isabelle/HOL, @{method standard} also takes classical rules into
-  account (cf.\ \secref{sec:classical}).
+  In Isabelle/HOL, @{method standard} also takes classical rules into account
+  (cf.\ \secref{sec:classical}).
 \<close>
 
 
 subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>
 
 text \<open>
-  The following proof methods and attributes refer to basic logical
-  operations of Isar.  Further methods and attributes are provided by
-  several generic and object-logic specific tools and packages (see
-  \chref{ch:gen-tools} and \partref{part:hol}).
+  The following proof methods and attributes refer to basic logical operations
+  of Isar. Further methods and attributes are provided by several generic and
+  object-logic specific tools and packages (see \chref{ch:gen-tools} and
+  \partref{part:hol}).
 
   \begin{matharray}{rcl}
     @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]
@@ -816,113 +768,103 @@
     @@{attribute "where"} @{syntax named_insts} @{syntax for_fixes}
   \<close>}
 
-  \<^descr> @{command "print_rules"} prints rules declared via attributes
-  @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
-  (Pure) dest} of Isabelle/Pure.
+  \<^descr> @{command "print_rules"} prints rules declared via attributes @{attribute
+  (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure) dest} of
+  Isabelle/Pure.
 
-  See also the analogous @{command "print_claset"} command for similar
-  rule declarations of the classical reasoner
-  (\secref{sec:classical}).
+  See also the analogous @{command "print_claset"} command for similar rule
+  declarations of the classical reasoner (\secref{sec:classical}).
 
-  \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as
-  premises into the goal, and nothing else.
+  \<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as premises
+  into the goal, and nothing else.
 
   Note that command @{command_ref "proof"} without any method actually
-  performs a single reduction step using the @{method_ref (Pure) rule}
-  method; thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command
-  "proof"}~\<open>-\<close>'' rather than @{command "proof"} alone.
+  performs a single reduction step using the @{method_ref (Pure) rule} method;
+  thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command "proof"}~\<open>-\<close>''
+  rather than @{command "proof"} alone.
 
-  \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals
-  into cases within the context (see also \secref{sec:cases-induct}). The
-  specified case names are used if present; otherwise cases are numbered
-  starting from 1.
+  \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals into cases
+  within the context (see also \secref{sec:cases-induct}). The specified case
+  names are used if present; otherwise cases are numbered starting from 1.
 
   Invoking cases in the subsequent proof body via the @{command_ref case}
   command will @{command fix} goal parameters, @{command assume} goal
   premises, and @{command let} variable @{variable_ref ?case} refer to the
   conclusion.
 
-  \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from
-  \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or implicitly from the current proof context)
-  modulo unification of schematic type and term variables.  The rule
-  structure is not taken into account, i.e.\ meta-level implication is
-  considered atomic.  This is the same principle underlying literal
-  facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
-  "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that
-  \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close> in the
-  proof context.
+  \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or
+  implicitly from the current proof context) modulo unification of schematic
+  type and term variables. The rule structure is not taken into account, i.e.\
+  meta-level implication is considered atomic. This is the same principle
+  underlying literal facts (cf.\ \secref{sec:syn-att}): ``@{command
+  "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
+  "note"}~\<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close>'' provided that \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close>
+  in the proof context.
 
-  \<^descr> @{method assumption} solves some goal by a single assumption
-  step.  All given facts are guaranteed to participate in the
-  refinement; this means there may be only 0 or 1 in the first place.
-  Recall that @{command "qed"} (\secref{sec:proof-steps}) already
-  concludes any remaining sub-goals by assumption, so structured
-  proofs usually need not quote the @{method assumption} method at
-  all.
+  \<^descr> @{method assumption} solves some goal by a single assumption step. All
+  given facts are guaranteed to participate in the refinement; this means
+  there may be only 0 or 1 in the first place. Recall that @{command "qed"}
+  (\secref{sec:proof-steps}) already concludes any remaining sub-goals by
+  assumption, so structured proofs usually need not quote the @{method
+  assumption} method at all.
 
-  \<^descr> @{method this} applies all of the current facts directly as
-  rules.  Recall that ``@{command "."}'' (dot) abbreviates ``@{command
-  "by"}~\<open>this\<close>''.
+  \<^descr> @{method this} applies all of the current facts directly as rules. Recall
+  that ``@{command "."}'' (dot) abbreviates ``@{command "by"}~\<open>this\<close>''.
 
-  \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as
-  argument in backward manner; facts are used to reduce the rule
-  before applying it to the goal.  Thus @{method (Pure) rule} without facts
-  is plain introduction, while with facts it becomes elimination.
+  \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as argument in
+  backward manner; facts are used to reduce the rule before applying it to the
+  goal. Thus @{method (Pure) rule} without facts is plain introduction, while
+  with facts it becomes elimination.
 
-  When no arguments are given, the @{method (Pure) rule} method tries to
-  pick appropriate rules automatically, as declared in the current context
-  using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute
-  (Pure) dest} attributes (see below). This is included in the standard
-  behaviour of @{command "proof"} and ``@{command ".."}'' (double-dot) steps
-  (see \secref{sec:proof-steps}).
+  When no arguments are given, the @{method (Pure) rule} method tries to pick
+  appropriate rules automatically, as declared in the current context using
+  the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute (Pure)
+  dest} attributes (see below). This is included in the standard behaviour of
+  @{command "proof"} and ``@{command ".."}'' (double-dot) steps (see
+  \secref{sec:proof-steps}).
 
-  \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
-  @{attribute (Pure) dest} declare introduction, elimination, and
-  destruct rules, to be used with method @{method (Pure) rule}, and similar
-  tools.  Note that the latter will ignore rules declared with
-  ``\<open>?\<close>'', while ``\<open>!\<close>''  are used most aggressively.
+  \<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and @{attribute
+  (Pure) dest} declare introduction, elimination, and destruct rules, to be
+  used with method @{method (Pure) rule}, and similar tools. Note that the
+  latter will ignore rules declared with ``\<open>?\<close>'', while ``\<open>!\<close>'' are used most
+  aggressively.
 
-  The classical reasoner (see \secref{sec:classical}) introduces its
-  own variants of these attributes; use qualified names to access the
-  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
-  "Pure.intro"}.
+  The classical reasoner (see \secref{sec:classical}) introduces its own
+  variants of these attributes; use qualified names to access the present
+  versions of Isabelle/Pure, i.e.\ @{attribute (Pure) "Pure.intro"}.
 
-  \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction,
-  elimination, or destruct rules.
+  \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, elimination, or
+  destruct rules.
 
-  \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all
-  of the given rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left
-  order, which means that premises stemming from the \<open>a\<^sub>i\<close>
-  emerge in parallel in the result, without interfering with each
-  other.  In many practical situations, the \<open>a\<^sub>i\<close> do not have
-  premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually
-  read as functional application (modulo unification).
+  \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all of the given rules
+  \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left order, which means that premises
+  stemming from the \<open>a\<^sub>i\<close> emerge in parallel in the result, without
+  interfering with each other. In many practical situations, the \<open>a\<^sub>i\<close> do not
+  have premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually read as
+  functional application (modulo unification).
 
-  Argument positions may be effectively skipped by using ``\<open>_\<close>''
-  (underscore), which refers to the propositional identity rule in the
-  Pure theory.
+  Argument positions may be effectively skipped by using ``\<open>_\<close>'' (underscore),
+  which refers to the propositional identity rule in the Pure theory.
 
-  \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional
-  instantiation of term variables.  The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are
-  substituted for any schematic variables occurring in a theorem from
-  left to right; ``\<open>_\<close>'' (underscore) indicates to skip a
-  position.  Arguments following a ``\<open>concl:\<close>'' specification
-  refer to positions of the conclusion of a rule.
+  \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional instantiation of term
+  variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are substituted for any schematic
+  variables occurring in a theorem from left to right; ``\<open>_\<close>'' (underscore)
+  indicates to skip a position. Arguments following a ``\<open>concl:\<close>''
+  specification refer to positions of the conclusion of a rule.
 
-  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
-  be specified: the instantiated theorem is exported, and these
-  variables become schematic (usually with some shifting of indices).
+  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified:
+  the instantiated theorem is exported, and these variables become schematic
+  (usually with some shifting of indices).
 
-  \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close>
-  performs named instantiation of schematic type and term variables
-  occurring in a theorem.  Schematic variables have to be specified on
-  the left-hand side (e.g.\ \<open>?x1.3\<close>).  The question mark may
-  be omitted if the variable name is a plain identifier without index.
-  As type instantiations are inferred from term instantiations,
-  explicit type instantiations are seldom necessary.
+  \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> performs named
+  instantiation of schematic type and term variables occurring in a theorem.
+  Schematic variables have to be specified on the left-hand side (e.g.\
+  \<open>?x1.3\<close>). The question mark may be omitted if the variable name is a plain
+  identifier without index. As type instantiations are inferred from term
+  instantiations, explicit type instantiations are seldom necessary.
 
-  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
-  be specified as for @{attribute "of"} above.
+  An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may be specified
+  as for @{attribute "of"} above.
 \<close>
 
 
@@ -937,14 +879,13 @@
     @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
 
-  \<^descr> @{command "method_setup"}~\<open>name = text description\<close>
-  defines a proof method in the current context.  The given \<open>text\<close> has to be an ML expression of type
-  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
-  basic parsers defined in structure @{ML_structure Args} and @{ML_structure
-  Attrib}.  There are also combinators like @{ML METHOD} and @{ML
-  SIMPLE_METHOD} to turn certain tactic forms into official proof
-  methods; the primed versions refer to tactics with explicit goal
-  addressing.
+  \<^descr> @{command "method_setup"}~\<open>name = text description\<close> defines a proof method
+  in the current context. The given \<open>text\<close> has to be an ML expression of type
+  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\ basic
+  parsers defined in structure @{ML_structure Args} and @{ML_structure
+  Attrib}. There are also combinators like @{ML METHOD} and @{ML
+  SIMPLE_METHOD} to turn certain tactic forms into official proof methods; the
+  primed versions refer to tactics with explicit goal addressing.
 
   Here are some example method definitions:
 \<close>
@@ -980,52 +921,47 @@
     @{attribute_def consumes} & : & \<open>attribute\<close> \\
   \end{matharray}
 
-  The puristic way to build up Isar proof contexts is by explicit
-  language elements like @{command "fix"}, @{command "assume"},
-  @{command "let"} (see \secref{sec:proof-context}).  This is adequate
-  for plain natural deduction, but easily becomes unwieldy in concrete
-  verification tasks, which typically involve big induction rules with
-  several cases.
+  The puristic way to build up Isar proof contexts is by explicit language
+  elements like @{command "fix"}, @{command "assume"}, @{command "let"} (see
+  \secref{sec:proof-context}). This is adequate for plain natural deduction,
+  but easily becomes unwieldy in concrete verification tasks, which typically
+  involve big induction rules with several cases.
 
-  The @{command "case"} command provides a shorthand to refer to a
-  local context symbolically: certain proof methods provide an
-  environment of named ``cases'' of the form \<open>c: x\<^sub>1, \<dots>,
-  x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of ``@{command
-  "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots>
-  \<phi>\<^sub>n\<close>''.  Term bindings may be covered as well, notably
-  @{variable ?case} for the main conclusion.
+  The @{command "case"} command provides a shorthand to refer to a local
+  context symbolically: certain proof methods provide an environment of named
+  ``cases'' of the form \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of
+  ``@{command "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
+  x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Term bindings may be covered as
+  well, notably @{variable ?case} for the main conclusion.
 
-  By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of
-  a case value is marked as hidden, i.e.\ there is no way to refer to
-  such parameters in the subsequent proof text.  After all, original
-  rule parameters stem from somewhere outside of the current proof
-  text.  By using the explicit form ``@{command "case"}~\<open>(c
-  y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to
-  chose local names that fit nicely into the current context.
+  By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of a case value is marked as
+  hidden, i.e.\ there is no way to refer to such parameters in the subsequent
+  proof text. After all, original rule parameters stem from somewhere outside
+  of the current proof text. By using the explicit form ``@{command
+  "case"}~\<open>(c y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to chose local
+  names that fit nicely into the current context.
 
   \<^medskip>
-  It is important to note that proper use of @{command
-  "case"} does not provide means to peek at the current goal state,
-  which is not directly observable in Isar!  Nonetheless, goal
-  refinement commands do provide named cases \<open>goal\<^sub>i\<close>
-  for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
-  Using this extra feature requires great care, because some bits of
-  the internal tactical machinery intrude the proof text.  In
-  particular, parameter names stemming from the left-over of automated
-  reasoning tools are usually quite unpredictable.
+  It is important to note that proper use of @{command "case"} does not
+  provide means to peek at the current goal state, which is not directly
+  observable in Isar! Nonetheless, goal refinement commands do provide named
+  cases \<open>goal\<^sub>i\<close> for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
+  Using this extra feature requires great care, because some bits of the
+  internal tactical machinery intrude the proof text. In particular, parameter
+  names stemming from the left-over of automated reasoning tools are usually
+  quite unpredictable.
 
   Under normal circumstances, the text of cases emerge from standard
-  elimination or induction rules, which in turn are derived from
-  previous theory specifications in a canonical way (say from
-  @{command "inductive"} definitions).
+  elimination or induction rules, which in turn are derived from previous
+  theory specifications in a canonical way (say from @{command "inductive"}
+  definitions).
 
   \<^medskip>
-  Proper cases are only available if both the proof method
-  and the rules involved support this.  By using appropriate
-  attributes, case names, conclusions, and parameters may be also
-  declared by hand.  Thus variant versions of rules that have been
-  derived manually become ready to use in advanced case analysis
-  later.
+  Proper cases are only available if both the proof method and the rules
+  involved support this. By using appropriate attributes, case names,
+  conclusions, and parameters may be also declared by hand. Thus variant
+  versions of rules that have been derived manually become ready to use in
+  advanced case analysis later.
 
   @{rail \<open>
     @@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')')
@@ -1039,67 +975,62 @@
     @@{attribute consumes} @{syntax int}?
   \<close>}
 
-  \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local
-  context \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an
-  appropriate proof method (such as @{method_ref cases} and @{method_ref
-  induct}). The command ``@{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>''
-  abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command
-  "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by the
-  prefix \<open>a\<close>, and all such facts are collectively bound to the name
-  \<open>a\<close>.
+  \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local context \<open>c:
+  x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an appropriate proof method (such
+  as @{method_ref cases} and @{method_ref induct}). The command ``@{command
+  "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots>
+  x\<^sub>m\<close>~@{command "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by
+  the prefix \<open>a\<close>, and all such facts are collectively bound to the name \<open>a\<close>.
 
-  The fact name is specification \<open>a\<close> is optional, the default is to
-  re-use \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same
-  as @{command "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
-
-  \<^descr> @{command "print_cases"} prints all local contexts of the
-  current state, using Isar proof language notation.
+  The fact name is specification \<open>a\<close> is optional, the default is to re-use
+  \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same as @{command
+  "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
 
-  \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for
-  the local contexts of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close>
-  refers to the \<^emph>\<open>prefix\<close> of the list of premises. Each of the
-  cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
-  the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close>
-  from left to right.
+  \<^descr> @{command "print_cases"} prints all local contexts of the current state,
+  using Isar proof language notation.
+
+  \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for the local contexts
+  of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> refers to the \<^emph>\<open>prefix\<close> of the list
+  of premises. Each of the cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
+  the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> from left to
+  right.
 
-  \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares
-  names for the conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix of arguments of a logical formula
-  built by nesting a binary connective (e.g.\ \<open>\<or>\<close>).
+  \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares names for the
+  conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix
+  of arguments of a logical formula built by nesting a binary connective
+  (e.g.\ \<open>\<or>\<close>).
 
-  Note that proof methods such as @{method induct} and @{method
-  coinduct} already provide a default name for the conclusion as a
-  whole.  The need to name subformulas only arises with cases that
-  split into several sub-cases, as in common co-induction rules.
+  Note that proof methods such as @{method induct} and @{method coinduct}
+  already provide a default name for the conclusion as a whole. The need to
+  name subformulas only arises with cases that split into several sub-cases,
+  as in common co-induction rules.
 
-  \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames
-  the innermost parameters of premises \<open>1, \<dots>, n\<close> of some
-  theorem.  An empty list of names may be given to skip positions,
-  leaving the present parameters unchanged.
+  \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames the innermost
+  parameters of premises \<open>1, \<dots>, n\<close> of some theorem. An empty list of names may
+  be given to skip positions, leaving the present parameters unchanged.
 
-  Note that the default usage of case rules does \<^emph>\<open>not\<close> directly
-  expose parameters to the proof context.
+  Note that the default usage of case rules does \<^emph>\<open>not\<close> directly expose
+  parameters to the proof context.
 
-  \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major
-  premises'' of a rule, i.e.\ the number of facts to be consumed when
-  it is applied by an appropriate proof method.  The default value of
-  @{attribute consumes} is \<open>n = 1\<close>, which is appropriate for
-  the usual kind of cases and induction rules for inductive sets (cf.\
-  \secref{sec:hol-inductive}).  Rules without any @{attribute
-  consumes} declaration given are treated as if @{attribute
+  \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major premises'' of a
+  rule, i.e.\ the number of facts to be consumed when it is applied by an
+  appropriate proof method. The default value of @{attribute consumes} is \<open>n =
+  1\<close>, which is appropriate for the usual kind of cases and induction rules for
+  inductive sets (cf.\ \secref{sec:hol-inductive}). Rules without any
+  @{attribute consumes} declaration given are treated as if @{attribute
   consumes}~\<open>0\<close> had been specified.
 
-  A negative \<open>n\<close> is interpreted relatively to the total number
-  of premises of the rule in the target context.  Thus its absolute
-  value specifies the remaining number of premises, after subtracting
-  the prefix of major premises as indicated above. This form of
-  declaration has the technical advantage of being stable under more
-  morphisms, notably those that export the result from a nested
-  @{command_ref context} with additional assumptions.
+  A negative \<open>n\<close> is interpreted relatively to the total number of premises of
+  the rule in the target context. Thus its absolute value specifies the
+  remaining number of premises, after subtracting the prefix of major premises
+  as indicated above. This form of declaration has the technical advantage of
+  being stable under more morphisms, notably those that export the result from
+  a nested @{command_ref context} with additional assumptions.
 
-  Note that explicit @{attribute consumes} declarations are only
-  rarely needed; this is already taken care of automatically by the
-  higher-level @{attribute cases}, @{attribute induct}, and
-  @{attribute coinduct} declarations.
+  Note that explicit @{attribute consumes} declarations are only rarely
+  needed; this is already taken care of automatically by the higher-level
+  @{attribute cases}, @{attribute induct}, and @{attribute coinduct}
+  declarations.
 \<close>
 
 
@@ -1113,25 +1044,23 @@
     @{method_def coinduct} & : & \<open>method\<close> \\
   \end{matharray}
 
-  The @{method cases}, @{method induct}, @{method induction},
-  and @{method coinduct}
-  methods provide a uniform interface to common proof techniques over
-  datatypes, inductive predicates (or sets), recursive functions etc.
-  The corresponding rules may be specified and instantiated in a
-  casual manner.  Furthermore, these methods provide named local
-  contexts that may be invoked via the @{command "case"} proof command
-  within the subsequent proof text.  This accommodates compact proof
-  texts even when reasoning about large specifications.
+  The @{method cases}, @{method induct}, @{method induction}, and @{method
+  coinduct} methods provide a uniform interface to common proof techniques
+  over datatypes, inductive predicates (or sets), recursive functions etc. The
+  corresponding rules may be specified and instantiated in a casual manner.
+  Furthermore, these methods provide named local contexts that may be invoked
+  via the @{command "case"} proof command within the subsequent proof text.
+  This accommodates compact proof texts even when reasoning about large
+  specifications.
 
-  The @{method induct} method also provides some additional
-  infrastructure in order to be applicable to structure statements
-  (either using explicit meta-level connectives, or including facts
-  and parameters separately).  This avoids cumbersome encoding of
-  ``strengthened'' inductive statements within the object-logic.
+  The @{method induct} method also provides some additional infrastructure in
+  order to be applicable to structure statements (either using explicit
+  meta-level connectives, or including facts and parameters separately). This
+  avoids cumbersome encoding of ``strengthened'' inductive statements within
+  the object-logic.
 
-  Method @{method induction} differs from @{method induct} only in
-  the names of the facts in the local context invoked by the @{command "case"}
-  command.
+  Method @{method induction} differs from @{method induct} only in the names
+  of the facts in the local context invoked by the @{command "case"} command.
 
   @{rail \<open>
     @@{method cases} ('(' 'no_simp' ')')? \<newline>
@@ -1154,13 +1083,12 @@
     taking: 'taking' ':' @{syntax insts}
   \<close>}
 
-  \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method
-  rule} with an appropriate case distinction theorem, instantiated to
-  the subjects \<open>insts\<close>.  Symbolic case names are bound according
-  to the rule's local contexts.
+  \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method rule} with an
+  appropriate case distinction theorem, instantiated to the subjects \<open>insts\<close>.
+  Symbolic case names are bound according to the rule's local contexts.
 
-  The rule is determined as follows, according to the facts and
-  arguments passed to the @{method cases} method:
+  The rule is determined as follows, according to the facts and arguments
+  passed to the @{method cases} method:
 
   \<^medskip>
   \begin{tabular}{llll}
@@ -1173,16 +1101,16 @@
   \end{tabular}
   \<^medskip>
 
-  Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close>
-  of premises of the case rule; within each premise, the \<^emph>\<open>prefix\<close>
-  of variables is instantiated.  In most situations, only a single
-  term needs to be specified; this refers to the first variable of the
-  last premise (it is usually the same for all cases).  The \<open>(no_simp)\<close> option can be used to disable pre-simplification of
-  cases (see the description of @{method induct} below for details).
+  Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> of premises
+  of the case rule; within each premise, the \<^emph>\<open>prefix\<close> of variables is
+  instantiated. In most situations, only a single term needs to be specified;
+  this refers to the first variable of the last premise (it is usually the
+  same for all cases). The \<open>(no_simp)\<close> option can be used to disable
+  pre-simplification of cases (see the description of @{method induct} below
+  for details).
 
-  \<^descr> @{method induct}~\<open>insts R\<close> and
-  @{method induction}~\<open>insts R\<close> are analogous to the
-  @{method cases} method, but refer to induction rules, which are
+  \<^descr> @{method induct}~\<open>insts R\<close> and @{method induction}~\<open>insts R\<close> are analogous
+  to the @{method cases} method, but refer to induction rules, which are
   determined as follows:
 
   \<^medskip>
@@ -1194,51 +1122,44 @@
   \end{tabular}
   \<^medskip>
 
-  Several instantiations may be given, each referring to some part of
-  a mutual inductive definition or datatype --- only related partial
-  induction rules may be used together, though.  Any of the lists of
-  terms \<open>P, x, \<dots>\<close> refers to the \<^emph>\<open>suffix\<close> of variables
-  present in the induction rule.  This enables the writer to specify
-  only induction variables, or both predicates and variables, for
-  example.
+  Several instantiations may be given, each referring to some part of a mutual
+  inductive definition or datatype --- only related partial induction rules
+  may be used together, though. Any of the lists of terms \<open>P, x, \<dots>\<close> refers to
+  the \<^emph>\<open>suffix\<close> of variables present in the induction rule. This enables the
+  writer to specify only induction variables, or both predicates and
+  variables, for example.
 
-  Instantiations may be definitional: equations \<open>x \<equiv> t\<close>
-  introduce local definitions, which are inserted into the claim and
-  discharged after applying the induction rule.  Equalities reappear
-  in the inductive cases, but have been transformed according to the
-  induction principle being involved here.  In order to achieve
-  practically useful induction hypotheses, some variables occurring in
-  \<open>t\<close> need to be fixed (see below).  Instantiations of the form
-  \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a
-  shorthand for \mbox{\<open>x \<equiv> t\<close>}, where \<open>x\<close> is a fresh
-  variable. If this is not intended, \<open>t\<close> has to be enclosed in
-  parentheses.  By default, the equalities generated by definitional
-  instantiations are pre-simplified using a specific set of rules,
-  usually consisting of distinctness and injectivity theorems for
-  datatypes. This pre-simplification may cause some of the parameters
-  of an inductive case to disappear, or may even completely delete
-  some of the inductive cases, if one of the equalities occurring in
-  their premises can be simplified to \<open>False\<close>.  The \<open>(no_simp)\<close> option can be used to disable pre-simplification.
-  Additional rules to be used in pre-simplification can be declared
-  using the @{attribute_def induct_simp} attribute.
+  Instantiations may be definitional: equations \<open>x \<equiv> t\<close> introduce local
+  definitions, which are inserted into the claim and discharged after applying
+  the induction rule. Equalities reappear in the inductive cases, but have
+  been transformed according to the induction principle being involved here.
+  In order to achieve practically useful induction hypotheses, some variables
+  occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form
+  \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,
+  where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be
+  enclosed in parentheses. By default, the equalities generated by
+  definitional instantiations are pre-simplified using a specific set of
+  rules, usually consisting of distinctness and injectivity theorems for
+  datatypes. This pre-simplification may cause some of the parameters of an
+  inductive case to disappear, or may even completely delete some of the
+  inductive cases, if one of the equalities occurring in their premises can be
+  simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable
+  pre-simplification. Additional rules to be used in pre-simplification can be
+  declared using the @{attribute_def induct_simp} attribute.
 
-  The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>''
-  specification generalizes variables \<open>x\<^sub>1, \<dots>,
-  x\<^sub>m\<close> of the original goal before applying induction.  One can
-  separate variables by ``\<open>and\<close>'' to generalize them in other
-  goals then the first. Thus induction hypotheses may become
-  sufficiently general to get the proof through.  Together with
-  definitional instantiations, one may effectively perform induction
-  over expressions of a certain structure.
+  The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
+  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
+  separate variables by ``\<open>and\<close>'' to generalize them in other goals then the
+  first. Thus induction hypotheses may become sufficiently general to get the
+  proof through. Together with definitional instantiations, one may
+  effectively perform induction over expressions of a certain structure.
 
-  The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
-  specification provides additional instantiations of a prefix of
-  pending variables in the rule.  Such schematic induction rules
-  rarely occur in practice, though.
+  The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
+  instantiations of a prefix of pending variables in the rule. Such schematic
+  induction rules rarely occur in practice, though.
 
-  \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the
-  @{method induct} method, but refers to coinduction rules, which are
-  determined as follows:
+  \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the @{method induct} method,
+  but refers to coinduction rules, which are determined as follows:
 
   \<^medskip>
   \begin{tabular}{llll}
@@ -1249,69 +1170,63 @@
   \end{tabular}
   \<^medskip>
 
-  Coinduction is the dual of induction.  Induction essentially
-  eliminates \<open>A x\<close> towards a generic result \<open>P x\<close>,
-  while coinduction introduces \<open>A x\<close> starting with \<open>B
-  x\<close>, for a suitable ``bisimulation'' \<open>B\<close>.  The cases of a
-  coinduct rule are typically named after the predicates or sets being
-  covered, while the conclusions consist of several alternatives being
-  named after the individual destructor patterns.
+  Coinduction is the dual of induction. Induction essentially eliminates \<open>A x\<close>
+  towards a generic result \<open>P x\<close>, while coinduction introduces \<open>A x\<close> starting
+  with \<open>B x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a coinduct
+  rule are typically named after the predicates or sets being covered, while
+  the conclusions consist of several alternatives being named after the
+  individual destructor patterns.
 
-  The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables
-  occurring in the rule's major premise, or conclusion if unavailable.
-  An additional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
-  specification may be required in order to specify the bisimulation
-  to be used in the coinduction step.
+  The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables occurring in
+  the rule's major premise, or conclusion if unavailable. An additional
+  ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification may be required in order to specify
+  the bisimulation to be used in the coinduction step.
 
 
   Above methods produce named local contexts, as determined by the
-  instantiated rule as given in the text.  Beyond that, the @{method
-  induct} and @{method coinduct} methods guess further instantiations
-  from the goal specification itself.  Any persisting unresolved
-  schematic variables of the resulting rule will render the the
-  corresponding case invalid.  The term binding @{variable ?case} for
-  the conclusion will be provided with each case, provided that term
-  is fully specified.
+  instantiated rule as given in the text. Beyond that, the @{method induct}
+  and @{method coinduct} methods guess further instantiations from the goal
+  specification itself. Any persisting unresolved schematic variables of the
+  resulting rule will render the the corresponding case invalid. The term
+  binding @{variable ?case} for the conclusion will be provided with each
+  case, provided that term is fully specified.
 
-  The @{command "print_cases"} command prints all named cases present
-  in the current proof state.
+  The @{command "print_cases"} command prints all named cases present in the
+  current proof state.
 
   \<^medskip>
-  Despite the additional infrastructure, both @{method cases}
-  and @{method coinduct} merely apply a certain rule, after
-  instantiation, while conforming due to the usual way of monotonic
-  natural deduction: the context of a structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close>
-  reappears unchanged after the case split.
+  Despite the additional infrastructure, both @{method cases} and @{method
+  coinduct} merely apply a certain rule, after instantiation, while conforming
+  due to the usual way of monotonic natural deduction: the context of a
+  structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close> reappears unchanged after
+  the case split.
 
-  The @{method induct} method is fundamentally different in this
-  respect: the meta-level structure is passed through the
-  ``recursive'' course involved in the induction.  Thus the original
-  statement is basically replaced by separate copies, corresponding to
-  the induction hypotheses and conclusion; the original goal context
-  is no longer available.  Thus local assumptions, fixed parameters
-  and definitions effectively participate in the inductive rephrasing
-  of the original statement.
+  The @{method induct} method is fundamentally different in this respect: the
+  meta-level structure is passed through the ``recursive'' course involved in
+  the induction. Thus the original statement is basically replaced by separate
+  copies, corresponding to the induction hypotheses and conclusion; the
+  original goal context is no longer available. Thus local assumptions, fixed
+  parameters and definitions effectively participate in the inductive
+  rephrasing of the original statement.
 
   In @{method induct} proofs, local assumptions introduced by cases are split
-  into two different kinds: \<open>hyps\<close> stemming from the rule and
-  \<open>prems\<close> from the goal statement.  This is reflected in the
-  extracted cases accordingly, so invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and \<open>c.prems\<close>,
-  as well as fact \<open>c\<close> to hold the all-inclusive list.
+  into two different kinds: \<open>hyps\<close> stemming from the rule and \<open>prems\<close> from the
+  goal statement. This is reflected in the extracted cases accordingly, so
+  invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and
+  \<open>c.prems\<close>, as well as fact \<open>c\<close> to hold the all-inclusive list.
 
   In @{method induction} proofs, local assumptions introduced by cases are
-  split into three different kinds: \<open>IH\<close>, the induction hypotheses,
-  \<open>hyps\<close>, the remaining hypotheses stemming from the rule, and
-  \<open>prems\<close>, the assumptions from the goal statement. The names are
-  \<open>c.IH\<close>, \<open>c.hyps\<close> and \<open>c.prems\<close>, as above.
-
+  split into three different kinds: \<open>IH\<close>, the induction hypotheses, \<open>hyps\<close>,
+  the remaining hypotheses stemming from the rule, and \<open>prems\<close>, the
+  assumptions from the goal statement. The names are \<open>c.IH\<close>, \<open>c.hyps\<close> and
+  \<open>c.prems\<close>, as above.
 
   \<^medskip>
-  Facts presented to either method are consumed according to
-  the number of ``major premises'' of the rule involved, which is
-  usually 0 for plain cases and induction rules of datatypes etc.\ and
-  1 for rules of inductive predicates or sets and the like.  The
-  remaining facts are inserted into the goal verbatim before the
-  actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
+  Facts presented to either method are consumed according to the number of
+  ``major premises'' of the rule involved, which is usually 0 for plain cases
+  and induction rules of datatypes etc.\ and 1 for rules of inductive
+  predicates or sets and the like. The remaining facts are inserted into the
+  goal verbatim before the actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
   applied.
 \<close>
 
@@ -1337,27 +1252,24 @@
     spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del'
   \<close>}
 
-  \<^descr> @{command "print_induct_rules"} prints cases and induct rules
-  for predicates (or sets) and types of the current context.
+  \<^descr> @{command "print_induct_rules"} prints cases and induct rules for
+  predicates (or sets) and types of the current context.
 
-  \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute
-  coinduct} (as attributes) declare rules for reasoning about
-  (co)inductive predicates (or sets) and types, using the
-  corresponding methods of the same name.  Certain definitional
-  packages of object-logics usually declare emerging cases and
+  \<^descr> @{attribute cases}, @{attribute induct}, and @{attribute coinduct} (as
+  attributes) declare rules for reasoning about (co)inductive predicates (or
+  sets) and types, using the corresponding methods of the same name. Certain
+  definitional packages of object-logics usually declare emerging cases and
   induction rules as expected, so users rarely need to intervene.
 
-  Rules may be deleted via the \<open>del\<close> specification, which
-  covers all of the \<open>type\<close>/\<open>pred\<close>/\<open>set\<close>
-  sub-categories simultaneously.  For example, @{attribute
-  cases}~\<open>del\<close> removes any @{attribute cases} rules declared for
-  some type, predicate, or set.
+  Rules may be deleted via the \<open>del\<close> specification, which covers all of the
+  \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> sub-categories simultaneously. For example, @{attribute
+  cases}~\<open>del\<close> removes any @{attribute cases} rules declared for some type,
+  predicate, or set.
 
-  Manual rule declarations usually refer to the @{attribute
-  case_names} and @{attribute params} attributes to adjust names of
-  cases and parameters of a rule; the @{attribute consumes}
-  declaration is taken care of automatically: @{attribute
-  consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
+  Manual rule declarations usually refer to the @{attribute case_names} and
+  @{attribute params} attributes to adjust names of cases and parameters of a
+  rule; the @{attribute consumes} declaration is taken care of automatically:
+  @{attribute consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
   consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules.
 \<close>
 
@@ -1371,11 +1283,11 @@
     @{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
   \end{matharray}
 
-  Generalized elimination means that hypothetical parameters and premises
-  may be introduced in the current context, potentially with a split into
-  cases. This works by virtue of a locally proven rule that establishes the
-  soundness of this temporary context extension. As representative examples,
-  one may think of standard rules from Isabelle/HOL like this:
+  Generalized elimination means that hypothetical parameters and premises may
+  be introduced in the current context, potentially with a split into cases.
+  This works by virtue of a locally proven rule that establishes the soundness
+  of this temporary context extension. As representative examples, one may
+  think of standard rules from Isabelle/HOL like this:
 
   \<^medskip>
   \begin{tabular}{ll}
@@ -1386,9 +1298,9 @@
   \<^medskip>
 
   In general, these particular rules and connectives need to get involved at
-  all: this concept works directly in Isabelle/Pure via Isar commands
-  defined below. In particular, the logic of elimination and case splitting
-  is delegated to an Isar proof, which often involves automated tools.
+  all: this concept works directly in Isabelle/Pure via Isar commands defined
+  below. In particular, the logic of elimination and case splitting is
+  delegated to an Isar proof, which often involves automated tools.
 
   @{rail \<open>
     @@{command consider} @{syntax obtain_clauses}
@@ -1399,21 +1311,21 @@
     @@{command guess} (@{syntax "fixes"} + @'and')
   \<close>}
 
-  \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
-  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case
-  splitting into separate subgoals, such that each case involves new
-  parameters and premises. After the proof is finished, the resulting rule
-  may be used directly with the @{method cases} proof method
-  (\secref{sec:cases-induct}), in order to perform actual case-splitting of
-  the proof text via @{command case} and @{command next} as usual.
+  \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
+  \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots>\<close> states a rule for case splitting
+  into separate subgoals, such that each case involves new parameters and
+  premises. After the proof is finished, the resulting rule may be used
+  directly with the @{method cases} proof method (\secref{sec:cases-induct}),
+  in order to perform actual case-splitting of the proof text via @{command
+  case} and @{command next} as usual.
 
-  Optional names in round parentheses refer to case names: in the proof of
-  the rule this is a fact name, in the resulting rule it is used as
-  annotation with the @{attribute_ref case_names} attribute.
+  Optional names in round parentheses refer to case names: in the proof of the
+  rule this is a fact name, in the resulting rule it is used as annotation
+  with the @{attribute_ref case_names} attribute.
 
   \<^medskip>
-  Formally, the command @{command consider} is defined as derived
-  Isar language element as follows:
+  Formally, the command @{command consider} is defined as derived Isar
+  language element as follows:
 
   \begin{matharray}{l}
     @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]
@@ -1426,25 +1338,24 @@
   \end{matharray}
 
   See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
-  statements, as well as @{command print_statement} to print existing rules
-  in a similar format.
+  statements, as well as @{command print_statement} to print existing rules in
+  a similar format.
 
-  \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close>
-  states a generalized elimination rule with exactly one case. After the
-  proof is finished, it is activated for the subsequent proof text: the
-  context is augmented via @{command fix}~\<open>\<^vec>x\<close> @{command
-  assume}~\<open>\<^vec>A \<^vec>x\<close>, with special provisions to export
-  later results by discharging these assumptions again.
+  \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> states a
+  generalized elimination rule with exactly one case. After the proof is
+  finished, it is activated for the subsequent proof text: the context is
+  augmented via @{command fix}~\<open>\<^vec>x\<close> @{command assume}~\<open>\<^vec>A
+  \<^vec>x\<close>, with special provisions to export later results by discharging
+  these assumptions again.
 
   Note that according to the parameter scopes within the elimination rule,
-  results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the
-  export will fail! This restriction conforms to the usual manner of
-  existential reasoning in Natural Deduction.
+  results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the export
+  will fail! This restriction conforms to the usual manner of existential
+  reasoning in Natural Deduction.
 
   \<^medskip>
-  Formally, the command @{command obtain} is defined as derived
-  Isar language element as follows, using an instrumented variant of
-  @{command assume}:
+  Formally, the command @{command obtain} is defined as derived Isar language
+  element as follows, using an instrumented variant of @{command assume}:
 
   \begin{matharray}{l}
     @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]
@@ -1462,23 +1373,23 @@
   \<^emph>\<open>improper\<close>.
 
   A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
-  subsequent refinement steps may turn this to anything of the form \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
-  subgoals. The final goal state is then used as reduction rule for the
-  obtain pattern described above. Obtained parameters \<open>\<^vec>x\<close> are
-  marked as internal by default, and thus inaccessible in the proof text.
-  The variable names and type constraints given as arguments for @{command
-  "guess"} specify a prefix of accessible parameters.
+  subsequent refinement steps may turn this to anything of the form
+  \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
+  subgoals. The final goal state is then used as reduction rule for the obtain
+  pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as
+  internal by default, and thus inaccessible in the proof text. The variable
+  names and type constraints given as arguments for @{command "guess"} specify
+  a prefix of accessible parameters.
 
 
-  In the proof of @{command consider} and @{command obtain} the local
-  premises are always bound to the fact name @{fact_ref that}, according to
-  structured Isar statements involving @{keyword_ref "if"}
-  (\secref{sec:goals}).
+  In the proof of @{command consider} and @{command obtain} the local premises
+  are always bound to the fact name @{fact_ref that}, according to structured
+  Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).
 
-  Facts that are established by @{command "obtain"} and @{command "guess"}
-  may not be polymorphic: any type-variables occurring here are fixed in the
-  present context. This is a natural consequence of the role of @{command
-  fix} and @{command assume} in these constructs.
+  Facts that are established by @{command "obtain"} and @{command "guess"} may
+  not be polymorphic: any type-variables occurring here are fixed in the
+  present context. This is a natural consequence of the role of @{command fix}
+  and @{command assume} in these constructs.
 \<close>
 
 end
diff -r cfabbc083977 -r 5b878bc6ae98 src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 14:49:30 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Fri Nov 13 15:06:58 2015 +0100
@@ -14,8 +14,8 @@
   Nonetheless, it is possible to emulate proof scripts by sequential
   refinements of a proof state in backwards mode, notably with the @{command
   apply} command (see \secref{sec:tactic-commands}). There are also various
-  proof methods that allow to refer to implicit goal state information that
-  is normally not accessible to structured Isar proofs (see
+  proof methods that allow to refer to implicit goal state information that is
+  normally not accessible to structured Isar proofs (see
   \secref{sec:tactics}).
 \<close>
 
@@ -43,44 +43,42 @@
     @@{command prefer} @{syntax nat}
   \<close>}
 
-  \<^descr> @{command "supply"} supports fact definitions during goal
-  refinement: it is similar to @{command "note"}, but it operates in
-  backwards mode and does not have any impact on chained facts.
+  \<^descr> @{command "supply"} supports fact definitions during goal refinement: it
+  is similar to @{command "note"}, but it operates in backwards mode and does
+  not have any impact on chained facts.
 
-  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in
-  initial position, but unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode.  Thus consecutive method applications may be
-  given just as in tactic scripts.
+  \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but
+  unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus
+  consecutive method applications may be given just as in tactic scripts.
 
-  Facts are passed to \<open>m\<close> as indicated by the goal's
-  forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards.  Thus any
-  further @{command "apply"} command would always work in a purely
-  backward manner.
+  Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and
+  are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command
+  would always work in a purely backward manner.
 
-  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal position.  Basically, this simulates a
-  multi-step tactic script for @{command "qed"}, but may be given
-  anywhere within the proof body.
+  \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal
+  position. Basically, this simulates a multi-step tactic script for @{command
+  "qed"}, but may be given anywhere within the proof body.
 
-  No facts are passed to \<open>m\<close> here.  Furthermore, the static
-  context is that of the enclosing goal (as for actual @{command
-  "qed"}).  Thus the proof method may not refer to any assumptions
-  introduced in the current body, for example.
+  No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of
+  the enclosing goal (as for actual @{command "qed"}). Thus the proof method
+  may not refer to any assumptions introduced in the current body, for
+  example.
 
-  \<^descr> @{command "done"} completes a proof script, provided that the
-  current goal state is solved completely.  Note that actual
-  structured proof commands (e.g.\ ``@{command "."}'' or @{command
-  "sorry"}) may be used to conclude proof scripts as well.
+  \<^descr> @{command "done"} completes a proof script, provided that the current goal
+  state is solved completely. Note that actual structured proof commands
+  (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude
+  proof scripts as well.
 
-  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close>
-  shuffle the list of pending goals: @{command "defer"} puts off
-  sub-goal \<open>n\<close> to the end of the list (\<open>n = 1\<close> by
-  default), while @{command "prefer"} brings sub-goal \<open>n\<close> to the
-  front.
+  \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of
+  pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the
+  list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to
+  the front.
 
-  \<^descr> @{command "back"} does back-tracking over the result sequence
-  of the latest proof command.  Any proof command may return multiple
-  results, and this command explores the possibilities step-by-step.
-  It is mainly useful for experimentation and interactive exploration,
-  and should be avoided in finished proofs.
+  \<^descr> @{command "back"} does back-tracking over the result sequence of the
+  latest proof command. Any proof command may return multiple results, and
+  this command explores the possibilities step-by-step. It is mainly useful
+  for experimentation and interactive exploration, and should be avoided in
+  finished proofs.
 \<close>
 
 
@@ -109,23 +107,22 @@
   structured proofs, but the text of the parameters, premises and conclusion
   is not given explicitly.
 
-  Goal parameters may be specified separately, in order to allow referring
-  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
-  y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
-  "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
-  latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
-  positions may be skipped via dummies (underscore). Unspecified names
-  remain internal, and thus inaccessible in the proof text.
+  Goal parameters may be specified separately, in order to allow referring to
+  them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>''
+  names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>''
+  names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol
+  as notation. Parameter positions may be skipped via dummies (underscore).
+  Unspecified names remain internal, and thus inaccessible in the proof text.
 
-  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that
-  goal premises should be turned into assumptions of the context (otherwise
-  the remaining conclusion is a Pure implication). The fact name and
-  attributes are optional; the particular name ``\<open>prems\<close>'' is a common
-  convention for the premises of an arbitrary goal context in proof scripts.
+  ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal
+  premises should be turned into assumptions of the context (otherwise the
+  remaining conclusion is a Pure implication). The fact name and attributes
+  are optional; the particular name ``\<open>prems\<close>'' is a common convention for the
+  premises of an arbitrary goal context in proof scripts.
 
-  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result
-  of a proven subgoal. Thus it may be re-used in further reasoning, similar
-  to the result of @{command show} in structured Isar proofs.
+  ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a
+  proven subgoal. Thus it may be re-used in further reasoning, similar to the
+  result of @{command show} in structured Isar proofs.
 
 
   Here are some abstract examples:
@@ -181,32 +178,29 @@
 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
 
 text \<open>
-  The following improper proof methods emulate traditional tactics.
-  These admit direct access to the goal state, which is normally
-  considered harmful!  In particular, this may involve both numbered
-  goal addressing (default 1), and dynamic instantiation within the
-  scope of some subgoal.
+  The following improper proof methods emulate traditional tactics. These
+  admit direct access to the goal state, which is normally considered harmful!
+  In particular, this may involve both numbered goal addressing (default 1),
+  and dynamic instantiation within the scope of some subgoal.
 
   \begin{warn}
-    Dynamic instantiations refer to universally quantified parameters
-    of a subgoal (the dynamic context) rather than fixed variables and
-    term abbreviations of a (static) Isar context.
+    Dynamic instantiations refer to universally quantified parameters of a
+    subgoal (the dynamic context) rather than fixed variables and term
+    abbreviations of a (static) Isar context.
   \end{warn}
 
-  Tactic emulation methods, unlike their ML counterparts, admit
-  simultaneous instantiation from both dynamic and static contexts.
-  If names occur in both contexts goal parameters hide locally fixed
-  variables.  Likewise, schematic variables refer to term
-  abbreviations, if present in the static context.  Otherwise the
-  schematic variable is interpreted as a schematic variable and left
-  to be solved by unification with certain parts of the subgoal.
+  Tactic emulation methods, unlike their ML counterparts, admit simultaneous
+  instantiation from both dynamic and static contexts. If names occur in both
+  contexts goal parameters hide locally fixed variables. Likewise, schematic
+  variables refer to term abbreviations, if present in the static context.
+  Otherwise the schematic variable is interpreted as a schematic variable and
+  left to be solved by unification with certain parts of the subgoal.
 
   Note that the tactic emulation proof methods in Isabelle/Isar are
-  consistently named \<open>foo_tac\<close>.  Note also that variable names
-  occurring on left hand sides of instantiations must be preceded by a
-  question mark if they coincide with a keyword or contain dots.  This
-  is consistent with the attribute @{attribute "where"} (see
-  \secref{sec:pure-meth-att}).
+  consistently named \<open>foo_tac\<close>. Note also that variable names occurring on
+  left hand sides of instantiations must be preceded by a question mark if
+  they coincide with a keyword or contain dots. This is consistent with the
+  attribute @{attribute "where"} (see \secref{sec:pure-meth-att}).
 
   \begin{matharray}{rcl}
     @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
@@ -239,52 +233,46 @@
   \<close>}
 
   \<^descr> @{method rule_tac} etc. do resolution of rules with explicit
-  instantiation.  This works the same way as the ML tactics @{ML
+  instantiation. This works the same way as the ML tactics @{ML
   Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
 
-  Multiple rules may be only given if there is no instantiation; then
-  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
-  @{cite "isabelle-implementation"}).
-
-  \<^descr> @{method cut_tac} inserts facts into the proof state as
-  assumption of a subgoal; instantiations may be given as well.  Note
-  that the scope of schematic variables is spread over the main goal
-  statement and rule premises are turned into new subgoals.  This is
-  in contrast to the regular method @{method insert} which inserts
-  closed rule statements.
+  Multiple rules may be only given if there is no instantiation; then @{method
+  rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite
+  "isabelle-implementation"}).
 
-  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise
-  from a subgoal.  Note that \<open>\<phi>\<close> may contain schematic
-  variables, to abbreviate the intended proposition; the first
-  matching subgoal premise will be deleted.  Removing useless premises
-  from a subgoal increases its readability and can make search tactics
-  run faster.
+  \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a
+  subgoal; instantiations may be given as well. Note that the scope of
+  schematic variables is spread over the main goal statement and rule premises
+  are turned into new subgoals. This is in contrast to the regular method
+  @{method insert} which inserts closed rule statements.
 
-  \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions
-  \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as local premises to a subgoal, and poses the same
-  as new subgoals (in the original context).
+  \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note
+  that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended
+  proposition; the first matching subgoal premise will be deleted. Removing
+  useless premises from a subgoal increases its readability and can make
+  search tactics run faster.
 
-  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a
-  goal according to the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the
-  \<^emph>\<open>suffix\<close> of variables.
+  \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as
+  local premises to a subgoal, and poses the same as new subgoals (in the
+  original context).
 
-  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a
-  subgoal by \<open>n\<close> positions: from right to left if \<open>n\<close> is
-  positive, and from left to right if \<open>n\<close> is negative; the
-  default value is 1.
+  \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to
+  the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables.
+
+  \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close>
+  positions: from right to left if \<open>n\<close> is positive, and from left to right if
+  \<open>n\<close> is negative; the default value is 1.
 
-  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from
-  any ML text of type @{ML_type tactic}.  Apart from the usual ML
-  environment and the current proof context, the ML code may refer to
-  the locally bound values @{ML_text facts}, which indicates any
-  current facts used for forward-chaining.
+  \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type
+  @{ML_type tactic}. Apart from the usual ML environment and the current proof
+  context, the ML code may refer to the locally bound values @{ML_text facts},
+  which indicates any current facts used for forward-chaining.
 
-  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but
-  presents the goal state in its raw internal form, where simultaneous
-  subgoals appear as conjunction of the logical framework instead of
-  the usual split into several subgoals.  While feature this is useful
-  for debugging of complex method definitions, it should not never
-  appear in production theories.
+  \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal
+  state in its raw internal form, where simultaneous subgoals appear as
+  conjunction of the logical framework instead of the usual split into several
+  subgoals. While feature this is useful for debugging of complex method
+  definitions, it should not never appear in production theories.
 \<close>
 
 end
\ No newline at end of file