Re: [isabelle] rewriting with assumptions from right to left
this is not precisely the answer you are looking for, but the following
proof script should also do the trick of proving the lemma:
by (cases a) auto
2010/11/11 Viorel Preoteasa <viorel.preoteasa at abo.fi>
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and