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

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?


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