--- 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 ***