[isabelle] primcorec does not terminate



Dear BNF experts,

In the attached theory, the primcorec definition of a function does not terminate (tested with both Isabelle2014 and Isabelle2015-RC0). Is is because my definition is erroneous or a shortcoming of the primcorec implementation?

Best,
Andreas

Attachment: Scratch.thy
Description: application/extension-thy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.