*To*: Victor Porton <porton at narod.ru>*Subject*: Re: [isabelle] Surprisingly this verifies*From*: Tjark Weber <webertj at in.tum.de>*Date*: Sat, 09 Jul 2011 15:18:29 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <324991310220372@web92.yandex.ru>*References*: <324991310220372@web92.yandex.ru>

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

**Follow-Ups**:**Re: [isabelle] Surprisingly this verifies***From:*Victor Porton

**Re: [isabelle] Surprisingly this verifies***From:*Victor Porton

**References**:**[isabelle] Surprisingly this verifies***From:*Victor Porton

- Previous by Date: [isabelle] Surprisingly this verifies
- Next by Date: Re: [isabelle] Surprisingly this verifies
- Previous by Thread: [isabelle] Surprisingly this verifies
- Next by Thread: Re: [isabelle] Surprisingly this verifies
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list