--- a/src/HOL/Real/Hyperreal/README.html Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/Hyperreal/README.html Thu Sep 21 12:11:38 2000 +0200
@@ -9,7 +9,39 @@
<LI><A HREF="Filter.html">Filter</A>
Theory of Filters and Ultrafilters.
-Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
+Main result is a version of the Ultrafilter Theorem proved using
+Zorn's Lemma.
+
+<LI><A HREF="HyperDef.html">HyperDef</A>
+Ultrapower construction of the hyperreals
+
+<LI><A HREF="NSA.html">NSA</A>
+Theory defining sets of infinite numbers, infinitesimals,
+the infinitely close relation, and their various algebraic properties.
+
+<LI><A HREF="HyperNat.html">HyperNat</A>
+Ultrapower construction of the hypernaturals
+
+<LI><A HREF="HyperPow.html">HyperPow</A>
+Powers theory for the hyperreals
+
+<LI><A HREF="Star.html">Star</A>
+Nonstandard extensions of real sets and real functions
+
+<LI><A HREF="NatStar.html">NatStar</A>
+Nonstandard extensions of sets of naturals and functions on the natural
+numbers
+
+<LI><A HREF="SEQ.html">SEQ</A>
+Theory of sequences developed using standard and nonstandard analysis
+
+<LI><A HREF="Lim.html">Lim</A>
+Theory of limits, continuous functions, and derivatives
+
+<LI><A HREF="Series.html">Series</A>
+Standard theory of finite summation and infinite series
+
+
</UL>
<P>Last modified on $Date$
@@ -21,3 +53,4 @@
</ADDRESS>
</BODY></HTML>
+