Re: [isabelle] Surprisingly this verifies
09.07.2011, 18:18, "Tjark Weber" <webertj at in.tum.de>:
> On Sat, 2011-07-09 at 18:06 +0400, Victor Porton wrote:
>> The following self-contradictory theory (Two definitions contradict to
>> each other.) verifies by Isabelle 2011. Where is the error?!
> Strange -- I get the following error message:
> *** Bad arguments on lhs: "(t1, x)"
> *** The error(s) above occurred in definition:
> *** "f (t1, x) \<equiv> t1"
> *** At command "definition"
> Two more remarks:
>> theory test
>> imports HOL Main
> There is no need to import HOL. In fact, you shouldn't. Simply
> importing Main will be sufficient.
>> definition "f (t1, x) = t1"
>> definition "f (t1, x) = t2"
> These definitions are not contradictory; they merely imply t1 = t2.
> Kind regards,
Oh, sorry, after restart of Emacs it does not verify. It is a bug in ProofGeneral.
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and