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
     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>
     8 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
     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