# HG changeset patch
# User haftmann
# Date 1293102269 -3600
# Node ID f5e14d6f5eba38963ccb6838439291d7d6ca6e38
# Parent  5379e4a85a667d18c3f9d37e9fac28ef97b95f1e
NEWS

diff -r 5379e4a85a66 -r f5e14d6f5eba NEWS
--- a/NEWS	Thu Dec 23 12:01:02 2010 +0100
+++ b/NEWS	Thu Dec 23 12:04:29 2010 +0100
@@ -197,9 +197,12 @@
 HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
 examples.
 
-* 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.
+* New command 'type_lifting' allows to register properties on
+the functorial structure of types.
+
+* Predicate "sorted" now defined inductively, with
+nice induction rules.  INCOMPATIBILITY: former sorted.simps now
+named sorted_simps.
 
 * Constant "contents" renamed to "the_elem", to free the generic name
 contents for other uses.  INCOMPATIBILITY.