--- a/NEWS Fri Jun 25 07:19:21 2010 +0200
+++ b/NEWS Mon Jun 28 15:32:06 2010 +0200
@@ -6,6 +6,22 @@
*** HOL ***
+* Dropped old infix syntax "mem" for List.member; use "in set"
+instead. INCOMPATIBILITY.
+
+* Refactoring of code-generation specific operations in List.thy
+
+ constants
+ null ~> List.null
+
+ facts
+ mem_iff ~> member_def
+ null_empty ~> null_def
+
+INCOMPATIBILITY. Note that these were not suppossed to be used
+regularly unless for striking reasons; their main purpose was code
+generation.
+
* Some previously unqualified names have been qualified:
types