Re: [isabelle] A proof for existential
On Aug 5, 2010 1:10pm, Tjark Weber <webertj at in.tum.de> wrote:
On Thu, 2010-08-05 at 11:19 +0100, John Munroe wrote:
> Thanks for the reply. What if ax2 was ax2 :"ALL x. (ALL y. x ~= y -->
> hx > hy) --> gx = 0", would the lemma follow from ax1 and ax2 then?
Yes; see the attached Isabelle theory for an automatic proof.
Thanks. Just curious, without using metis, what would a manual proof look
This archive was generated by a fusion of
Pipermail (Mailman edition) and