# HG changeset patch
# User blanchet
# Date 1288094781 -7200
# Node ID a6a34e0313bbd12c3d452acacf0961829a6a6ea4
# Parent  0ea94d19af0835f9212d1dfba2cda1eab5ec1493# Parent  91b4b73dbafbc543fa742e4a7f1ff2949f606b3f
merged

diff -r 91b4b73dbafb -r a6a34e0313bb NEWS
--- a/NEWS	Tue Oct 26 13:50:57 2010 +0200
+++ b/NEWS	Tue Oct 26 14:06:21 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.