NEWS
changeset 58740 cb9d84d3e7f2
parent 58716 23a380cc45f4
child 58759 e55fe82f3803
--- a/NEWS	Tue Oct 21 17:23:16 2014 +0200
+++ b/NEWS	Tue Oct 21 21:10:44 2014 +0200
@@ -51,10 +51,9 @@
   dvd_plus_eq_left ~> dvd_add_left_iff
 Minor INCOMPATIBILITY.
 
-* More foundational definition for predicate "even":
+* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
   even_def ~> even_iff_mod_2_eq_zero
-  even_iff_2_dvd ~> even_def
-Minor INCOMPATIBILITY.
+INCOMPATIBILITY.
 
 * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
 Minor INCOMPATIBILITY.