[isabelle] rewriting with assumptions from right to left



Hello,

I have the following lemma:

lemma "fst a = a1 ==> snd a = a2 ==> a = (a1, a2)";

This will be automatically proved by using the assumptions from
right to left.

Is there a way of simplifying using the assumptions from right
to left?

Best regards,

Viorel





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