NEWS
changeset 39077 ee78849c1624
parent 38864 4abe644fcea5
child 39079 bddc3d3f6e53
--- a/NEWS	Thu Sep 02 11:54:09 2010 +0200
+++ b/NEWS	Thu Sep 02 13:32:17 2010 +0200
@@ -204,6 +204,9 @@
 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.
 
 *** FOL ***