Re: [isabelle] Problem with arbitrary specification in double inductive rule induction
Why is m1 still free even though I have specified that it should be
arbitrary? Including m1 in the arbitrary specification makes no
however removing m from the specification does make m free (as
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