src/HOL/Real/Hyperreal/README.html
changeset 5979 11cbf236ca16
child 5981 ec5c3d17969f
equal deleted inserted replaced
5978:fa2c2dd74f8c 5979:11cbf236ca16
       
     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