--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/README.html	Sun Dec 31 15:12:27 2000 +0100
@@ -0,0 +1,59 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
+
+<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
+<LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
+Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
+<UL>
+
+<UL>
+<LI><A HREF="Zorn.html">Zorn</A>
+Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
+
+<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. 
+
+<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$
+
+<HR>
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
+
+