NEWS
changeset 39754 150f831ce4a3
parent 39689 78b185bf7660
child 39771 553f9b9aed28
     1.1 --- a/NEWS	Tue Sep 28 09:43:13 2010 +0200
     1.2 +++ b/NEWS	Tue Sep 28 09:54:07 2010 +0200
     1.3 @@ -236,6 +236,9 @@
     1.4  generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
     1.5  The theorems bij_def and surj_def are unchanged.
     1.6  
     1.7 +* Function package: .psimps rules are no longer implicitly declared [simp].
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  *** FOL ***
    1.11  
    1.12  * All constant names are now qualified.  INCOMPATIBILITY.