Re: [isabelle] Sort constraints in the termination relation

Hi again,

> 2. To users of the function package: Can you give me an example of a
> function that uses class axioms to prove termination? Or possibly
> requires a "fundef_cong" rule with a sort constraint?

looking a bit further, I also found a fundef-cong-rule which contains
sort-constraints, namely sum.cong.

Look at AFP/Bernoulli/Bernoulli.thy, function bernoulli.


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