NEWS
changeset 31726 ffd2dc631d88
parent 31720 d1ac3f3b2f54
parent 31723 f5cafe803b55
child 31784 bd3486c57ba3
     1.1 --- a/NEWS	Fri Jun 19 20:22:46 2009 +0200
     1.2 +++ b/NEWS	Fri Jun 19 21:08:07 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  * NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
    1.18  If possible, use NewNumberTheory, not NumberTheory.
    1.19