*To*: jeremy at rsise.anu.edu.au*Subject*: Re: [isabelle] Finite set datatype?*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 08 Oct 2010 10:29:23 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4CAE5DFA.1060604@netspeed.com.au>*References*: <4CAC4CC3.3020506@it.uu.se> <20101006103854.8EC41492313@talisker.in.tum.de> <4CAD0FDD.5000001@rsise.anu.edu.au> <AANLkTikuQjAJsHmfHJSbcJ9QKyODEcqpntTGPMkBcu+Q@mail.gmail.com> <4CAE5DFA.1060604@netspeed.com.au>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Jeremy,

This "instantiation" command looks rather like the "instance" command -is that right?but it seems to have definitions following it rather than before it.Do you know whether its use is documented anywhere (and if so where) (Ican't find it now, probably because I only have Isabelle2005 installedhere now).

You can always find documentation on the latest release at

So I can't really see how it would work - would you be able to define atype class that encompasses sets and finite sets, and enables you todefine the power set function Pow, and get all the relevant theoremsabout it ?

Alex

**References**:**[isabelle] Finite set datatype?***From:*Palle Raabjerg

**[isabelle] Finite set datatype?***From:*Christian Urban

**Re: [isabelle] Finite set datatype?***From:*Jeremy Dawson

**Re: [isabelle] Finite set datatype?***From:*Brian Huffman

**Re: [isabelle] Finite set datatype?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Finite set datatype?
- Next by Date: [isabelle] Research Associate. DYVERSE: A New Kind of Control for Hybrid Systems
- Previous by Thread: Re: [isabelle] Finite set datatype?
- Next by Thread: Re: [isabelle] Finite set datatype?
- Cl-isabelle-users October 2010 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