Re: [isabelle] Problem with arbitrary specification in double inductive rule induction



Hi,

Yes it does. Thank you.

Mark

On 14 June 2018 at 21:07, Lars Hupel <hupel at in.tum.de> wrote:

> Hi Mark,
>
> Why is m1 still free even though I have specified that it should be
>> arbitrary? Including m1 in the arbitrary specification makes no difference
>> however removing m from the specification does make m free (as expected).
>>
>
> try this:
>
> proof(induction arbitrary: m and m1 rule: P_Q.inducts)
>
> Does that yield the proof state that you expected?
>
> Cheers
> Lars
>



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