NEWS
changeset 39916 8c83139a1433
parent 39910 10097e0a9dbd
child 39963 626b1d360d42
     1.1 --- a/NEWS	Mon Oct 04 12:22:58 2010 +0200
     1.2 +++ b/NEWS	Mon Oct 04 14:46:48 2010 +0200
     1.3 @@ -74,6 +74,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Predicates `distinct` and `sorted` now defined inductively, with nice
     1.8 +induction rules.  INCOMPATIBILITY: former distinct.simps and sorted.simps
     1.9 +now named distinct_simps and sorted_simps.
    1.10 +
    1.11  * Constant `contents` renamed to `the_elem`, to free the generic name
    1.12  contents for other uses.  INCOMPATIBILITY.
    1.13