diff -r 3417c1b91e3c -r c8cd5348c76d NEWS
--- a/NEWS	Mon Sep 26 20:39:18 2011 +0200
+++ b/NEWS	Mon Sep 26 20:53:53 2011 +0200
@@ -76,11 +76,6 @@
 
 *** HOL ***
 
-* New proof method "induction" that gives induction hypotheses the name IH,
-thus distinguishing them from further hypotheses that come from rule
-induction.  The latter are still called "hyps".  Method "induction" is a thin
-wrapper around "induct" and follows the same syntax.
-
 * Class bot and top require underlying partial order rather than
 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
@@ -93,8 +88,8 @@
 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,
 Sup_fun_def, Inf_apply, Sup_apply.
 
-Removed redundant lemmas (the right hand side gives hints how to replace them
-for (metis ...), or (simp only: ...) proofs):
+Removed redundant lemmas (the right hand side gives hints how to
+replace them for (metis ...), or (simp only: ...) proofs):
 
   Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
   Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
@@ -288,6 +283,12 @@
 
 * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
 
+* New proof method "induction" that gives induction hypotheses the
+name "IH", thus distinguishing them from further hypotheses that come
+from rule induction.  The latter are still called "hyps".  Method
+"induction" is a thin wrapper around "induct" and follows the same
+syntax.
+
 * Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is
 still available as a legacy feature for some time.