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