Re: [isabelle] Sort constraints in the termination relation
> 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