Open
Description
We should now, given Michael's work on cardinals, be able to support recursion on the right hand side of a function arrow, and possibly some of the other things supported by the datatype package in Isabelle/HOL. See http://sourceforge.net/p/hol/mailman/hol-developers/thread/B678E335-C741-4F09-8803-187E00BCFD92%40nicta.com.au/#msg34282410
There is a $5 open bounty on this issue. Add to the bounty at Bountysource.