changeset 41510 | 75c6c4069938 |
parent 41509 | c86889cf295b |
child 41512 | 8445396e1e39 |
--- a/NEWS Tue Jan 11 17:59:35 2011 +0100 +++ b/NEWS Tue Jan 11 18:23:29 2011 +0100 @@ -178,7 +178,7 @@ * Datatype package: theorems generated for executable equality (class eq) carry proper names and are treated as default code equations. -* New command 'type_lifting' allows to register properties on +* New command 'enriched_type' allows to register properties of the functorial structure of types. * Weaker versions of the "meson" and "metis" proof methods are now