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.