* 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. Alex