NEWS
changeset 17092 16971afe75f6
parent 17047 e2e2d75bb37b
child 17095 669005f73b81
--- 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.