*To*: Chris Osborn <cosborn3 at uiuc.edu>*Subject*: Re: [isabelle] proving finite universe*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Mon, 20 Oct 2008 09:36:19 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <2661ce380810191136i4f0e5347le014a9147bd67789@mail.gmail.com>*References*: <2661ce380810191136i4f0e5347le014a9147bd67789@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.17 (Macintosh/20080914)

Chris,

Best, Stephan Chris Osborn wrote:

Does anyone know how I can prove the following: "not (finite (UNIV::string set))" I have been unable to find applicable lemmas. Thanks in advance, Chris

begin:vcard fn:Stephan Merz n:Merz;Stephan org:INRIA Nancy & LORIA adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France email;internet:Stephan.Merz at loria.fr tel;work:(+33) 354 95 84 78 tel;fax:(+33) 383 41 30 79 x-mozilla-html:FALSE url:http://www.loria.fr/~merz/ version:2.1 end:vcard

**References**:**[isabelle] proving finite universe***From:*Chris Osborn

- Previous by Date: [isabelle] ALICS workshop at LPAR
- Next by Date: Re: [isabelle] proving finite universe
- Previous by Thread: Re: [isabelle] proving finite universe
- Next by Thread: Re: [isabelle] proving finite universe
- Cl-isabelle-users October 2008 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