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


Yes it does. Thank you.


On 14 June 2018 at 21:07, Lars Hupel <hupel at> 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.