*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Defining Union Types*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Date*: Tue, 26 Jul 2011 09:04:15 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4E2E53A8.7090705@in.tum.de>*References*: <CAAPnxw1oeghO4nx43XsDD4z4X5ZW2D02ejnfK=vLb_JEx=Bz2A@mail.gmail.com> <4E2E53A8.7090705@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:5.0) Gecko/20110707 Thunderbird/5.0

cheers chris On 07/26/2011 07:42 AM, Tobias Nipkow wrote:

It is written "+" and defined in theory Sum_Type, which is part of Main. It is hardly advertised because in most cases it is nicer to define your own special datatype. Tobias Am 26/07/2011 03:57, schrieb Alfio Martini:Dear Isabelle Users, Do we have in Isabelle something like a union (sum) type constructor with the corresponding injections? I went through the tutorial and did not find use or reference to it. If there is, can anyone point to an application or a written example of this? I assume there must be a simple way to do it. Many thanks!

**Follow-Ups**:**Re: [isabelle] Defining Union Types***From:*Alfio Martini

**References**:**[isabelle] Defining Union Types***From:*Alfio Martini

**Re: [isabelle] Defining Union Types***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Defining Union Types
- Next by Date: Re: [isabelle] Stuck with existential quantifier
- Previous by Thread: Re: [isabelle] Defining Union Types
- Next by Thread: Re: [isabelle] Defining Union Types
- 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