src/HOL/Real/Hyperreal/README.html
author paulson
Fri Nov 27 16:46:01 1998 +0100 (1998-11-27)
changeset 5981 ec5c3d17969f
parent 5979 11cbf236ca16
child 10043 a0364652e115
permissions -rw-r--r--
fixed a link
paulson@5979
     1
<!-- $Id$ -->
paulson@5979
     2
<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
paulson@5979
     3
paulson@5979
     4
<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
paulson@5979
     5
paulson@5979
     6
<UL>
paulson@5979
     7
<LI><A HREF="Zorn.html">Zorn</A>
paulson@5981
     8
Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
paulson@5979
     9
paulson@5979
    10
<LI><A HREF="Filter.html">Filter</A>
paulson@5979
    11
Theory of Filters and Ultrafilters.
paulson@5979
    12
Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
paulson@5979
    13
</UL>
paulson@5979
    14
paulson@5979
    15
<P>Last modified on $Date$
paulson@5979
    16
paulson@5979
    17
<HR>
paulson@5979
    18
paulson@5979
    19
<ADDRESS>
paulson@5979
    20
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
paulson@5979
    21
</ADDRESS>
paulson@5979
    22
</BODY></HTML>
paulson@5979
    23