| changeset 32989 | c28279b29ff1 |
| parent 32984 | 2ef1adff7eee |
| parent 32988 | d1d4d7a08a66 |
| child 32992 | 2318ff5fca1a |
--- a/NEWS Sun Oct 18 00:10:20 2009 +0200 +++ b/NEWS Sun Oct 18 12:07:56 2009 +0200 @@ -149,6 +149,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.