[isabelle] Eisbach match drule



Dear Eisbach developers,

I ran into a problem when using drule in match. It seems that drule is not supported, but rule is. For example, let's first define a silly lemma here:

lemma dummy: "A â B â B"
by auto

Then, when proving the following lemma, I try:

lemma "A â B â A â B"
apply (match premises in "A â B" â âdrule dummyâ)

But Isabelle says "Failed to apply proof method". However, the following is ok:

lemma "A â B â A â B"
apply (drule dummy)

Is there a way to use drule inside match? Or, is there an alternative to drule?

Thanks a lot,

Zhe




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