[isabelle-dev] NEWS

Alexander Krauss krauss at in.tum.de
Tue Oct 26 14:01:04 CEST 2010

* 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


More information about the isabelle-dev mailing list