Re: [isabelle] apply x apply y vs. by x y

On 27.07.2015 22:30, Lars Hupel wrote:
> the proof fails. Unfortunately I haven't been able to distill a small
> example exhibiting this behaviour. Now, I know that "by x y" is
> equivalent to "proof x qed y", but I always thought that is in turn
> equivalent to "apply x apply y".

It is not. I am not sure about proof, but qed usually does a bit more
than apply (e.g., solve things by assumption).

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