--- a/src/HOL/Hyperreal/README.html Wed Apr 21 13:18:37 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-<!-- $Id$ -->
-<HTML><HEAD>
- <TITLE>HOL/Hyperreal/README</TITLE>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- </HEAD><BODY>
-
-<H2>Hyperreal: Ultrafilter Construction of the Non-Standard Reals</H2>
-See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
-Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
-
-
- <UL>
- <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="HLog.html">HLog</A> Non-standard logarithms
- <li><a href="HSeries.html">HSeries</a> Non-standard theory of finite summation and infinite series
- <li><a href="HTranscendental.html">HTranscendental</a> Non-standard extensions of transcendental functions
- <LI><A HREF="HyperDef.html">HyperDef</A>
-Ultrapower construction of the hyperreals
-
-
- <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="IntFloor.html">IntFloor</a> Floor and Ceiling functions relating the reals and integers
- <li><a href="Integration.html">Integration</a> Gage integrals
- <li><a href="Lim.html">Lim</a> Theory of limits, continuous functions, and derivatives
-
- <LI><a href="Log.html">Log</a> Logarithms for the reals
-
- <li><a href="MacLaurin.html">MacLaurin</a> MacLaurin series
-
- <li><a href="NatStar.html">NatStar</a> Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals
- <li><a href="NthRoot.html">NthRoot</a> Existence of n-th roots of real numbers
- <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="Poly.html">Poly</a> Univariate real polynomials
- <li><a href="SEQ.html">SEQ</a> Convergence of sequences and series using standard and nonstandard analysis
- <li><a href="Series.html">Series</a> Finite summation and infinite series for the reals
- <li><a href="Star.html">Star</a> Nonstandard extensions of real sets and real functions
- <li><a href="Transcendental.html">Transcendental</a> Power series and transcendental functions
- </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>
--- a/src/HOL/Real/README.html Wed Apr 21 13:18:37 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<!-- $Id$ -->
-
-<html>
-
- <head>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <title>HOL/Real/README</title>
- </head>
-
- <body>
- <h2>Real: Dedekind Cut Construction of the Real Line</h2>
- <ul>
- <li><a href="Lubs.html">Lubs</a> Definition of upper bounds, lubs and so on, to support completeness proofs.
- <li><a href="PReal.html">PReal</a> The positive reals constructed using Dedekind cuts
-
- <li><a href="Rational.html">Rational</a> The rational numbers constructed as equivalence classes of integers
-
- <li><a href="RComplete.html">RComplete</a> The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
-
- <li><a href="RealDef.html">RealDef</a> The real numbers, their ordering properties, and embedding of the integers and the natural numbers
-
- <li><a href="RealPow.html">RealPow</a> Real numbers raised to natural number powers
-
- </ul>
- <p>Last modified on $Date$</p>
- <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>
\ No newline at end of file