Re: [isabelle] Case names qualified by locale

On 09/03/2015 02:16 PM, Lars Noschinski wrote:
> I don't know why the case names are lost here, but you should be able to
> use the names by using
>   L.P.coinduct[case_names P Q R]
> or maybe
>   L.P.coinduct[consumes 1, case_names P Q R]
> as a workaround.

Thanks, this works great.  I didn't know you could use [case_names] there.


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