*To*: Martin Klebermaß <martin at klebermass.de>*Subject*: Re: [isabelle] why does this definition work with wrong types*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 26 Jan 2007 18:51:51 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1D1AEA3F-F349-42BF-82D9-2D468E534370@klebermass.de>*References*: <45B84DAF.3030306@rsise.anu.edu.au> <2331ED73-85B1-407E-BC34-B8F280887280@cam.ac.uk> <1D1AEA3F-F349-42BF-82D9-2D468E534370@klebermass.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Martin Klebermaß wrote:

Hello,during review of my theorems i found a wrong definition of a set in mydefinition.For better reading i introduced a syntax for my defined sets.In one case i introduced a wrong definition of the syntax i used a natlist instead of a nat.So why does this definition work, because i think it should not work (anat list is mapped to a nat)theory syntaxdef imports Main begin consts typing :: "(nat * nat * nat * nat) set" syntax"_typing" :: "[nat,nat,nat list,nat] \<Rightarrow> bool" ("_;_

Tobias

**References**:**[isabelle] mod_add1_eq - Theory Divides***From:*SrinivasaRao Subramanya

**Re: [isabelle] mod_add1_eq - Theory Divides***From:*Lawrence Paulson

**[isabelle] why does this definition work with wrong types***From:*Martin Klebermaß

- Previous by Date: [isabelle] why does this definition work with wrong types
- Next by Date: [isabelle] 2nd CFP: Workshop on Invariant Generation (WING 2007), RISC, Hagenberg, Austria, 25-26 June, 2007
- Previous by Thread: [isabelle] why does this definition work with wrong types
- Next by Thread: [isabelle] IFM2007 Final call for contributions
- Cl-isabelle-users January 2007 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