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



Dear list,

I have a proof state which can be solved by the subsequent application
of two methods, i.e.

  have "P x"
    apply (induct x)
    apply auto
    done

If I rewrite this to

  have "P x"
    by (induct x) auto

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". Funnily enough, "by (x, y)" works. The
chained facts appear not to be significant here (I tried some variations).

Cheers
Lars




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