changeset 58645 | 94bef115c08f |
parent 58634 | 9f10d82e8188 |
child 58649 | a62065b5e1e2 |
--- a/NEWS Fri Oct 10 18:23:59 2014 +0200 +++ b/NEWS Thu Oct 09 22:43:48 2014 +0200 @@ -42,6 +42,10 @@ *** HOL *** +* More foundational definition for predicate "even": + even_def ~> even_iff_mod_2_eq_zero +Minor INCOMPATIBILITY. + * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1 Minor INCOMPATIBILITY.