author | hoelzl |
Thu, 02 Sep 2010 13:32:17 +0200 | |
changeset 39077 | ee78849c1624 |
parent 39076 | b3a9b6734663 |
child 39078 | 39f8f6d1eb74 |
--- 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 ***