src/HOL/Real/Hyperreal/README.html
changeset 10043 a0364652e115
parent 5981 ec5c3d17969f
child 10055 2264bdd8becc
     1.1 --- a/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -9,7 +9,39 @@
     1.4  
     1.5  <LI><A HREF="Filter.html">Filter</A>
     1.6  Theory of Filters and Ultrafilters.
     1.7 -Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
     1.8 +Main result is a version of the Ultrafilter Theorem proved using
     1.9 +Zorn's Lemma. 
    1.10 +
    1.11 +<LI><A HREF="HyperDef.html">HyperDef</A>
    1.12 +Ultrapower construction of the hyperreals
    1.13 +
    1.14 +<LI><A HREF="NSA.html">NSA</A>
    1.15 +Theory defining sets of infinite numbers, infinitesimals, 
    1.16 +the infinitely close relation, and their various algebraic properties.
    1.17 +
    1.18 +<LI><A HREF="HyperNat.html">HyperNat</A>
    1.19 +Ultrapower construction of the hypernaturals
    1.20 +
    1.21 +<LI><A HREF="HyperPow.html">HyperPow</A>
    1.22 +Powers theory for the hyperreals
    1.23 +
    1.24 +<LI><A HREF="Star.html">Star</A>
    1.25 +Nonstandard extensions of real sets and real functions
    1.26 +
    1.27 +<LI><A HREF="NatStar.html">NatStar</A>
    1.28 +Nonstandard extensions of sets of naturals and functions on the natural
    1.29 +numbers
    1.30 +
    1.31 +<LI><A HREF="SEQ.html">SEQ</A>
    1.32 +Theory of sequences developed using standard and nonstandard analysis
    1.33 +
    1.34 +<LI><A HREF="Lim.html">Lim</A>
    1.35 +Theory of limits, continuous functions, and derivatives
    1.36 +
    1.37 +<LI><A HREF="Series.html">Series</A>
    1.38 +Standard theory of finite summation and infinite series
    1.39 +
    1.40 +
    1.41  </UL>
    1.42  
    1.43  <P>Last modified on $Date$
    1.44 @@ -21,3 +53,4 @@
    1.45  </ADDRESS>
    1.46  </BODY></HTML>
    1.47  
    1.48 +