Re: [isabelle] rewriting with assumptions from right to left



Hi Viorel,

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

best regards,
Simon

2010/11/11 Viorel Preoteasa <viorel.preoteasa at abo.fi>

> 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.