# HG changeset patch
# User haftmann
# Date 1161615395 -7200
# Node ID 6a0cdb6f72d386806b037f42f5ddb6ca8656fbd5
# Parent  d0d8a48ae4e68dfcd4df94483e1ea1f5a39dd6e9
(added entry)

diff -r d0d8a48ae4e6 -r 6a0cdb6f72d3 NEWS
--- a/NEWS	Mon Oct 23 16:49:21 2006 +0200
+++ b/NEWS	Mon Oct 23 16:56:35 2006 +0200
@@ -475,6 +475,14 @@
 
 *** HOL ***
 
+* Constant "List.list_all2" in List.thy now uses authentic syntax.
+INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar
+level, use abbreviations instead.
+
+* Constant "List.op mem" in List.thy now has proper name: "List.memberl"
+INCOMPATIBILITY: rarely occuring name references (e.g. ``List.op mem.simps'')
+require renaming (e.g. ``List.memberl.simps'').
+
 * Renamed constants in HOL.thy:
     0      ~> HOL.zero
     1      ~> HOL.one