1.1 --- a/src/HOL/Isar_Examples/Summation.thy	Mon Nov 12 22:09:52 2012 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Summation.thy	Thu Nov 15 14:04:23 2012 +0100
     1.3 @@ -120,23 +120,17 @@
     1.4    finally show "?P (Suc n)" by simp
     1.5  qed
     1.6  
     1.7 -text {* Comparing these examples with the tactic script version
     1.8 -  @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference
     1.9 -  of how induction vs.\ simplification is
    1.10 -  applied.  While \cite[\S10]{isabelle-ref} advises for these examples
    1.11 -  that ``induction should not be applied until the goal is in the
    1.12 -  simplest form'' this would be a very bad idea in our setting.
    1.13 +text {* Note that in contrast to older traditions of tactical proof
    1.14 +  scripts, the structured proof applies induction on the original,
    1.15 +  unsimplified statement.  This allows to state the induction cases
    1.16 +  robustly and conveniently.  Simplification (or other automated)
    1.17 +  methods are then applied in terminal position to solve certain
    1.18 +  sub-problems completely.
    1.19  
    1.20 -  Simplification normalizes all arithmetic expressions involved,
    1.21 -  producing huge intermediate goals.  With applying induction
    1.22 -  afterwards, the Isar proof text would have to reflect the emerging
    1.23 -  configuration by appropriate sub-proofs.  This would result in badly
    1.24 -  structured, low-level technical reasoning, without any good idea of
    1.25 -  the actual point.
    1.26 -
    1.27 -  \medskip As a general rule of good proof style, automatic methods
    1.28 -  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used
    1.29 -  as initial proof methods, but only as terminal ones, solving certain
    1.30 -  goals completely.  *}
    1.31 +  As a general rule of good proof style, automatic methods such as
    1.32 +  $\idt{simp}$ or $\idt{auto}$ should normally be never used as
    1.33 +  initial proof methods with a nested sub-proof to address the
    1.34 +  automatically produced situation, but only as terminal ones to solve
    1.35 +  sub-problems.  *}
    1.36  
    1.37  end