--- a/NEWS Wed Nov 24 10:52:02 2010 +0100
+++ b/NEWS Mon Nov 22 10:34:33 2010 +0100
@@ -291,9 +291,10 @@
derive instantiated and simplified equations for inductive predicates,
similar to inductive_cases.
-* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
-generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
-The theorems bij_def and surj_def are unchanged.
+* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
+abbreviation of "range f = UIV". The theorems bij_def and surj_def are
+unchanged.
+INCOMPATIBILITY.
* Function package: .psimps rules are no longer implicitly declared [simp].
INCOMPATIBILITY.