--- a/src/HOL/Complex/README.html Mon Apr 19 12:17:58 2004 +0200
+++ b/src/HOL/Complex/README.html Mon Apr 19 13:49:35 2004 +0200
@@ -1,14 +1,25 @@
-<HTML><HEAD><TITLE>HOL/Complex/README</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ </HEAD><BODY>
-<H1>Complex--The Complex Numbers</H1>
-
-<P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
+<H1>Complex: The Complex Numbers</H1>
+ <P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
with numeric constants and some complex analysis. The development includes
nonstandard analysis for the complex numbers. Note that the image
<KBD>HOL-Complex</KBD> includes theories from the directories
-<KBD>HOL/Real</KBD> and <KBD>HOL/Hyperreal</KBD>.
+<KBD><a href="../Real/">HOL/Real</a></KBD> and <KBD><a href="../Hyperreal/">HOL/Hyperreal</a></KBD>.
+
-<HR>
+ <ul>
+ <li><a href="CLim.html">CLim</a> Limits, continuous functions, and derivatives for the complex numbers
+ <li><a href="CSeries.html">CSeries</a> Finite summation and infinite series for the complex numbers
+ <li><a href="CStar.html">CStar</a> Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
+ <li><a href="Complex.html">Complex</a> The complex numbers
+ <li><a href="NSCA.html">NSCA</a> Nonstandard complex analysis
+ <li><a href="NSComplex.html">NSComplex</a> Ultrapower construction of the nonstandard complex numbers
+ <li><a href="NSInduct.html">NSInduct</a> Nonstandard induction for the hypernatural numbers
+ </ul>
+ <HR>
<P>Last modified $Date$
</HTML>
--- a/src/HOL/Hyperreal/README.html Mon Apr 19 12:17:58 2004 +0200
+++ b/src/HOL/Hyperreal/README.html Mon Apr 19 13:49:35 2004 +0200
@@ -1,53 +1,51 @@
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
+<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>
+<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="Zorn.html">Zorn</A>
-Zorn's Lemma: proof based on the ZF version.
-<LI><A HREF="Filter.html">Filter</A>
+ <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="HyperDef.html">HyperDef</A>
+
+ <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="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="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$
-<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>
+ <HR>
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
--- a/src/HOL/Real/README.html Mon Apr 19 12:17:58 2004 +0200
+++ b/src/HOL/Real/README.html Mon Apr 19 13:49:35 2004 +0200
@@ -1,87 +1,30 @@
<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
-
-<H2>Real--Dedekind Cut Construction of the Real Line</H2>
-<ul>
-<LI><A HREF="PNat.html">PNat</A> The positive integers (very much the same as <A HREF="../Nat.html">Nat.thy</A>!)
-<LI><A HREF="PRat.html">PRat</A> The positive rationals
-<LI><A HREF="PReal.html">PReal</A> The positive reals constructed using Dedekind cuts
-<LI><A HREF="RealDef.html">RealDef</A> The real numbers
-<LI><A HREF="RealOrd.html">RealOrd</A> More real numbers theorems- ordering
-properties
-<LI><A HREF="RealInt.html">RealInt</A> Embedding of the integers in the reals
-<LI><A HREF="RealBin.html">RealBin</A> Binary arithmetic for the reals
+<html>
-<LI><A HREF="Lubs.html">Lubs</A> Definition of upper bounds, lubs and so on.
- (Useful e.g. in Fleuriot's NSA theory)
-<LI><A HREF="RComplete.html">RComplete</A> Proof of completeness of reals in form of the supremum
- property. Also proofs that the reals have the Archimedean
- property.
-<LI><A HREF="RealAbs.html">RealAbs</A> The absolute value function defined for the reals
-</ul>
-
-<H2>Hyperreal--Ultrapower Construction of the Non-Standard Reals</H2>
+ <head>
+ <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
+ <title>HOL/Real/README</title>
+ </head>
-<p>
-See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
-Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
-</p>
-
-<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
+ <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="HyperOrd.html">HyperOrd</A>
-More hyperreal numbers theorems- ordering properties
-
-<LI><A HREF="HRealAbs.html">HRealAbs</A> The absolute value function
-defined for 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="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="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
+ <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>
-
-
-</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>
+</html>
\ No newline at end of file