*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Tue, 08 Nov 2011 09:35:38 -0600*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAMej=27FtAe6=BikbdFRMdFMAzPSV3paVBaEjskLsE0TzEzdWw@mail.gmail.com>*References*: <4EB2E13B.507@gmx.com> <CAMej=25im4emE5QFAxDduhCbEkfLuu9r2YDi4P0hd2w=-9_qMg@mail.gmail.com> <4EB42510.7020408@gmx.com> <CAMej=248dGYvfRCFOK+L0JtyvmDeF-eEoA-f9a-XEro6+yMSew@mail.gmail.com> <4EB5709A.3090203@gmx.com> <CAMej=25frc7c9CUTVHqrQKiJ0AbHVy21spKBVkbEX46GrbCbpg@mail.gmail.com> <4EB81E84.8090606@gmx.com> <CAMej=27FtAe6=BikbdFRMdFMAzPSV3paVBaEjskLsE0TzEzdWw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

The function type operator (the "=>" we were using before) is primitive, that is, not created by type definition. In the usual model of HOL in set theory, it constructs function spaces.

Ramana, Makes sense, I guess. And even in src/ZF/ZF.thy I see that primitive.

Thanks, James

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: [isabelle] induction over mutually-inductively-defined predicate
- Previous by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 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