src/HOL/Real/Hyperreal/README.html
changeset 10755 0fb476ff855c
parent 10754 9bc30e51144c
child 10756 831c864cc56e
equal deleted inserted replaced
10754:9bc30e51144c 10755:0fb476ff855c
     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 <LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
       
     6 Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
       
     7 <UL>
       
     8 
       
     9 <UL>
       
    10 <LI><A HREF="Zorn.html">Zorn</A>
       
    11 Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
       
    12 
       
    13 <LI><A HREF="Filter.html">Filter</A>
       
    14 Theory of Filters and Ultrafilters.
       
    15 Main result is a version of the Ultrafilter Theorem proved using
       
    16 Zorn's Lemma. 
       
    17 
       
    18 <LI><A HREF="HyperDef.html">HyperDef</A>
       
    19 Ultrapower construction of the hyperreals
       
    20 
       
    21 <LI><A HREF="NSA.html">NSA</A>
       
    22 Theory defining sets of infinite numbers, infinitesimals, 
       
    23 the infinitely close relation, and their various algebraic properties.
       
    24 
       
    25 <LI><A HREF="HyperNat.html">HyperNat</A>
       
    26 Ultrapower construction of the hypernaturals
       
    27 
       
    28 <LI><A HREF="HyperPow.html">HyperPow</A>
       
    29 Powers theory for the hyperreals
       
    30 
       
    31 <LI><A HREF="Star.html">Star</A>
       
    32 Nonstandard extensions of real sets and real functions
       
    33 
       
    34 <LI><A HREF="NatStar.html">NatStar</A>
       
    35 Nonstandard extensions of sets of naturals and functions on the natural
       
    36 numbers
       
    37 
       
    38 <LI><A HREF="SEQ.html">SEQ</A>
       
    39 Theory of sequences developed using standard and nonstandard analysis
       
    40 
       
    41 <LI><A HREF="Lim.html">Lim</A>
       
    42 Theory of limits, continuous functions, and derivatives
       
    43 
       
    44 <LI><A HREF="Series.html">Series</A>
       
    45 Standard theory of finite summation and infinite series
       
    46 
       
    47 
       
    48 </UL>
       
    49 
       
    50 <P>Last modified on $Date$
       
    51 
       
    52 <HR>
       
    53 
       
    54 <ADDRESS>
       
    55 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
       
    56 </ADDRESS>
       
    57 </BODY></HTML>
       
    58 
       
    59