Re: [isabelle] function (tailrec,sequential) fails

Hi Joachim,

These problems with "tailrec" are starting to become embarrasing for me. :-}

theory Tmp imports Main

function (sequential,tailrec) f where "f True = 0"
  apply pat_completeness
  apply auto

gives me:

*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** f_sumC False = undefined
*** At command "done".

I just pushed a quick fix, which seems to help here, and also makes your real example go through:

The patch also works for the Isabelle2009-2 release.

Hope this helps...


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