| changeset 39250 | 548a3e5521ab |
| parent 39215 | 7b2631c91a95 |
| child 39277 | f263522ab226 |
--- a/NEWS Thu Sep 09 11:10:44 2010 +0200 +++ b/NEWS Thu Sep 09 14:38:14 2010 +0200 @@ -71,6 +71,8 @@ *** HOL *** +* String.literal is a type, but not a datatype. INCOMPATIBILITY. + * Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff * Renamed class eq and constant eq (for code generation) to class equal