*To*: Tom Ridge <tjr22 at cam.ac.uk>*Subject*: Re: [isabelle] Possible unsoundness in axclass mechanism*From*: Steven Obua <obua at in.tum.de>*Date*: Thu, 15 Sep 2005 11:46:55 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43285186.30502@cam.ac.uk>*References*: <43285186.30502@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; U; SunOS sun4u; en-US; rv:1.7.3) Gecko/20040915

Tom Ridge wrote:

theory False = Main: axclass blurg < type blurg: "! x. x ~= x" lemma l: "(x ~= (x::'a::blurg)) ==> False" apply(simp) done lemma "False" apply(rule l[of "x"]) apply(simp only: blurg) apply(simp) done endIs this supposed to happen? I thought declaring an axclass wassupposed to be a conservative extension.T

### Pending sort hypotheses: blurg

ML {* thm "L2" *} This will result in the following output: val it = "False" [.] : Thm.thm

-- Steven Obua

**References**:**[isabelle] Possible unsoundness in axclass mechanism***From:*Tom Ridge

- Previous by Date: [isabelle] Possible unsoundness in axclass mechanism
- Next by Date: Re: [isabelle] Possible unsoundness in axclass mechanism
- Previous by Thread: [isabelle] Possible unsoundness in axclass mechanism
- Next by Thread: Re: [isabelle] Possible unsoundness in axclass mechanism
- Cl-isabelle-users September 2005 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