| changeset 31790 | 05c92381363c |
| parent 31784 | bd3486c57ba3 |
| child 31804 | 627d142fce19 |
--- a/NEWS Tue Jun 23 21:07:39 2009 +0200 +++ b/NEWS Wed Jun 24 09:41:14 2009 +0200 @@ -43,6 +43,11 @@ * Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions Set.Pow_def and Set.image_def. INCOMPATIBILITY. +* Renamed theorems: +Suc_eq_add_numeral_1 -> Suc_eq_plus1 +Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left +Suc_plus1 -> Suc_eq_plus1 + * Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.: DatatypePackage ~> Datatype