diff -r e4fbe44838dd -r 0ea94d19af08 NEWS
--- a/NEWS	Tue Oct 26 13:17:37 2010 +0200
+++ b/NEWS	Tue Oct 26 13:50:18 2010 +0200
@@ -76,6 +76,13 @@
 
 *** HOL ***
 
+* New command 'partial_function' provides basic support for recursive
+function definitons over complete partial orders. Concrete instances
+are provided for i) the option type, ii) tail recursion on arbitrary
+types, and iii) the heap monad of Imperative_HOL. See
+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.