Re: [isabelle] Induction rule for partial_function (tailrec)

Hi Andreas,

Do you think
this should be the default induction rule for (tailrec)? Currently,
partial_function (tailrec) generates no induction rule at all. If so, I
can adapt Partial_Function.thy accordingly.

Yes, go ahead! This rule should be the default.


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