Re: [isabelle] Surprisingly this verifies
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and