NEWS

--- a/NEWS	Mon Oct 04 12:22:58 2010 +0200
+++ b/NEWS	Mon Oct 04 14:46:48 2010 +0200
@@ -74,6 +74,10 @@
 
 *** HOL ***
 
+* Predicates `distinct` and `sorted` now defined inductively, with nice
+induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
+now named distinct_simps and sorted_simps.
+
 * Constant `contents` renamed to `the_elem`, to free the generic name
 contents for other uses.  INCOMPATIBILITY.