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