--- a/NEWS Fri Jun 19 20:22:46 2009 +0200
+++ b/NEWS Fri Jun 19 21:08:07 2009 +0200
@@ -43,6 +43,16 @@
* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
Set.Pow_def and Set.image_def. INCOMPATIBILITY.
+* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
+
+ DatatypePackage ~> Datatype
+ InductivePackage ~> Inductive
+
+ etc.
+
+INCOMPATIBILITY.
+
+
* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
If possible, use NewNumberTheory, not NumberTheory.