| 5979 |      1 | <!-- $Id$ -->
 | 
|  |      2 | <HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
 | 
|  |      3 | 
 | 
|  |      4 | <H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
 | 
|  |      5 | 
 | 
|  |      6 | <UL>
 | 
|  |      7 | <LI><A HREF="Zorn.html">Zorn</A>
 | 
| 5981 |      8 | Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
 | 
| 5979 |      9 | 
 | 
|  |     10 | <LI><A HREF="Filter.html">Filter</A>
 | 
|  |     11 | Theory of Filters and Ultrafilters.
 | 
|  |     12 | Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
 | 
|  |     13 | </UL>
 | 
|  |     14 | 
 | 
|  |     15 | <P>Last modified on $Date$
 | 
|  |     16 | 
 | 
|  |     17 | <HR>
 | 
|  |     18 | 
 | 
|  |     19 | <ADDRESS>
 | 
|  |     20 | <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
 | 
|  |     21 | </ADDRESS>
 | 
|  |     22 | </BODY></HTML>
 | 
|  |     23 | 
 |