--- a/NEWS Thu Oct 31 11:44:20 2013 +0100
+++ b/NEWS Thu Oct 31 11:44:20 2013 +0100
@@ -6,9 +6,14 @@
*** HOL ***
-* Fact name generalization and consolidation:
- neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
-
+* Fact generalization and consolidation:
+ neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
+INCOMPATIBILITY.
+
+* Purely algebraic definition of even. Fact generalization and consolidation:
+ nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
+ even_zero_(nat|int) ~> even_zero
+INCOMPATIBILITY.
New in Isabelle2013-1 (November 2013)