*To*: Michal Czardybon <mczard at poczta.onet.pl>*Subject*: Re: [isabelle] I can't understand types in set-membership expressions*From*: Slawomir Kolodynski <skokodyn at yahoo.com>*Date*: Mon, 15 Sep 2008 15:08:48 -0700 (PDT)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <48CD4D07.3070407@poczta.onet.pl>*Reply-to*: skokodyn at yahoo.com

> You suggest me reading about Isabelle/ZF rather that /HOL, > but if so, > then why HOL is the main system in Isabelle. Isabelle is mostly used for tasks related to software verification, not formalized mathematics. HOL is much better for that. A more interesting question is why people choose to do formalized mathematics in Isabelle/HOL rather than Isabelle/ZF. For that I don't have a good answer. > Isn't > there a problem with > ZF that it doesn't solve the Russel's Paradox? Certainly not, see http://en.wikipedia.org/wiki/Zermelo_Fraenkel_set_theory . Slawomir

**Follow-Ups**:**Re: [isabelle] I can't understand types in set-membership expressions***From:*Lawrence Paulson

**References**:**Re: [isabelle] I can't understand types in set-membership expressions***From:*Michal Czardybon

- Previous by Date: Re: [isabelle] metis method and +-combinator
- Next by Date: Re: [isabelle] Giving a symbolic name to a tactical
- Previous by Thread: Re: [isabelle] I can't understand types in set-membership expressions
- Next by Thread: Re: [isabelle] I can't understand types in set-membership expressions
- Cl-isabelle-users September 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