# HG changeset patch
# User nipkow
# Date 1124281157 -7200
# Node ID 16971afe75f6bf94e8c40bf3b1bb3d0bb3ede4e1
# Parent  13593aa6a546f6f060e0a1b499fca341aea69892
*** empty log message ***

diff -r 13593aa6a546 -r 16971afe75f6 NEWS
--- a/NEWS	Wed Aug 17 13:52:53 2005 +0200
+++ b/NEWS	Wed Aug 17 14:19:17 2005 +0200
@@ -386,6 +386,16 @@
 
 * Theory Parity: added rules for simplifying exponents.
 
+* Theory List:
+
+The following theorems have been eliminated or modified
+(INCOMPATIBILITY):
+
+  list_all_Nil       now named list_all.simps(1)
+  list_all_Cons      now named list_all.simps(2)
+  list_all_conv      now named list_all_iff
+  set_mem_eq         now named mem_iff
+
 * Theories SetsAndFunctions and BigO (see HOL/Library) support
 asymptotic "big O" calculations.  See the notes in BigO.thy.