NEWS
changeset 39079 bddc3d3f6e53
parent 38980 af73cf0dc31f
parent 39077 ee78849c1624
child 39105 3b9e020c3908
     1.1 --- a/NEWS	Thu Sep 02 17:02:00 2010 +0200
     1.2 +++ b/NEWS	Thu Sep 02 18:45:23 2010 +0200
     1.3 @@ -200,6 +200,9 @@
     1.4  derive instantiated and simplified equations for inductive predicates,
     1.5  similar to inductive_cases.
     1.6  
     1.7 +* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
     1.8 +generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
     1.9 +The theorems bij_def and surj_def are unchanged.
    1.10  
    1.11  *** FOL ***
    1.12