diff -r c8a590599cb5 -r 05c92381363c NEWS
--- 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