NEWS
changeset 31723 f5cafe803b55
parent 31643 b040f1679f77
child 31726 ffd2dc631d88
     1.1 --- a/NEWS	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/NEWS	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -43,6 +43,16 @@
     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 +* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
     1.8 +
     1.9 +    DatatypePackage ~> Datatype
    1.10 +    InductivePackage ~> Inductive
    1.11 +
    1.12 +    etc.
    1.13 +
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16 +
    1.17  
    1.18  *** ML ***
    1.19