NEWS
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: