# HG changeset patch
# User wenzelm
# Date 1132774176 -3600
# Node ID 7607500220da06b0f79817e8da17e141cde31e69
# Parent  251bda68ba36b6bdf53dc4e24b43e77015f3e6f9
tuned;

diff -r 251bda68ba36 -r 7607500220da NEWS
--- a/NEWS	Wed Nov 23 18:52:05 2005 +0100
+++ b/NEWS	Wed Nov 23 20:29:36 2005 +0100
@@ -70,8 +70,7 @@
 work analogously.
 
 This is how to ``strengthen'' an inductive goal wrt. certain
-parameters (the scope of the internal generalization is both the goal
-and any additional facts being inserted before induction):
+parameters:
 
   lemma
     fixes n :: nat and x :: 'a
@@ -83,14 +82,14 @@
     show ?case sorry
   next
     case (Suc n x)
-    note `!!x. A n x ==> P n x` -- {* induction hypotheses, according to induction rule *}
-    note `A (Suc n) x`          -- {* induction premises, stemming from fact a *}
+    note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
+    note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
     show ?case sorry
   qed
 
 This is how to perform induction over ``expressions of a certain
 form'', using a locally defined inductive parameter n == "a x"
-together with strengthening (the latter is usually required to
+together with strengthening (the latter is usually required to get
 sufficiently flexible induction hypotheses).
 
   lemma