Re: [isabelle] Surprisingly this verifies




09.07.2011, 18:18, "Tjark Weber" <webertj at in.tum.de>:
> Victor,
>
> 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,
> Tjark

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