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.

Christoph




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