| changeset 39079 | bddc3d3f6e53 |
| parent 38980 | af73cf0dc31f |
| parent 39077 | ee78849c1624 |
| child 39105 | 3b9e020c3908 |
--- a/NEWS Thu Sep 02 17:02:00 2010 +0200 +++ b/NEWS Thu Sep 02 18:45:23 2010 +0200 @@ -200,6 +200,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 ***