diff -r 7b0ccc20cddc -r 250f487b3034 NEWS
--- a/NEWS	Mon Jun 07 17:13:36 2010 +0200
+++ b/NEWS	Mon Jun 07 17:52:30 2010 +0200
@@ -469,6 +469,17 @@
     "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
   - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
 
+* Method "induct" now takes instantiations of the form t, where t is not
+  a variable, as a shorthand for "x == t", where x is a fresh variable.
+  If this is not intended, t has to be enclosed in parentheses.
+  By default, the equalities generated by definitional instantiations
+  are pre-simplified, which may cause parameters of inductive cases
+  to disappear, or may even delete some of the inductive cases.
+  Use "induct (no_simp)" instead of "induct" to restore the old
+  behaviour. The (no_simp) option is also understood by the "cases"
+  and "nominal_induct" methods, which now perform pre-simplification, too.
+  INCOMPATIBILITY.
+
 
 *** HOLCF ***