| changeset 31723 | f5cafe803b55 |
| parent 31643 | b040f1679f77 |
| child 31726 | ffd2dc631d88 |
--- a/NEWS Thu Jun 18 18:31:14 2009 -0700 +++ b/NEWS Fri Jun 19 17:23:21 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. + + *** ML ***