Re: [isabelle] rewriting with assumptions from right to left
Viorel Preoteasa schrieb:
> 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?
We are getting a bit specialized here, aren't we?
Sledgehammering this goal yields
by (metis surjective_pairing).
> Best regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and