diff -r ec6dfd9ce573 -r 150f831ce4a3 NEWS
--- a/NEWS	Tue Sep 28 09:43:13 2010 +0200
+++ b/NEWS	Tue Sep 28 09:54:07 2010 +0200
@@ -236,6 +236,9 @@
 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
 The theorems bij_def and surj_def are unchanged.
 
+* Function package: .psimps rules are no longer implicitly declared [simp].
+INCOMPATIBILITY.
+
 *** FOL ***
 
 * All constant names are now qualified.  INCOMPATIBILITY.