| changeset 32988 | d1d4d7a08a66 |
| parent 32898 | e871d897969c |
| child 32989 | c28279b29ff1 |
--- a/NEWS Sat Oct 17 13:46:55 2009 +0200 +++ b/NEWS Sun Oct 18 12:07:25 2009 +0200 @@ -146,6 +146,10 @@ this. Fix using O_assoc[symmetric]. The same applies to the curried version "R OO S". +* Function "Inv" is renamed to "inv_onto" and function "inv" is now an +abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly. +INCOMPATIBILITY. + * ML antiquotation @{code_datatype} inserts definition of a datatype generated by the code generator; see Predicate.thy for an example.