Re: [isabelle] Termination of Recursive Function with Set Comprehension



On Thu, 2013-02-07 at 12:27 +0100, Johannes Hölzl wrote:
> With
> 
>   declare rev_conj_cong[fundef_cong]
> 
> your version also works.

Indeed it does. Many thanks!

Best regards,
Tjark






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