changeset 54890 | cb892d835803 |
parent 54881 | dff57132cf18 |
child 54893 | 4061ec8adb1c |
--- a/NEWS Wed Jan 01 01:05:46 2014 +0100 +++ b/NEWS Wed Jan 01 01:05:48 2014 +0100 @@ -33,6 +33,12 @@ *** HOL *** +* "declare [[code abort: …]]" replaces "code_abort …". +INCOMPATIBILITY. + +* "declare [[code drop: …]]" drops all code equations associated +with the given constants. + * Abolished slightly odd global lattice interpretation for min/max. Fact consolidations: