Re: [isabelle] Sort constraints in the termination relation

sum.cong is a great example, thanks!


On 12 April 2017 16:50:33 CEST, "Thiemann, Rene" <Rene.Thiemann at> wrote:
>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.