# HG changeset patch
# User paulson
# Date 1082546403 -7200
# Node ID b82a837f6959a61e0922220ace86d9c00be8d213
# Parent ffb4099c316f94314d06c2dfbd61c5718805d756
now included in Complex/README.html
diff -r ffb4099c316f -r b82a837f6959 src/HOL/Hyperreal/README.html
--- 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 @@
-
-
- HOL/Hyperreal/README
-
-
-
-Hyperreal: Ultrafilter Construction of the Non-Standard Reals
-See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real
-Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
-
-
-
- - Filter
-Theory of Filters and Ultrafilters.
-Main result is a version of the Ultrafilter Theorem proved using
-Zorn's Lemma.
-
-
-
- HLog Non-standard logarithms
-
- HSeries Non-standard theory of finite summation and infinite series
-
- HTranscendental Non-standard extensions of transcendental functions
-
- HyperDef
-Ultrapower construction of the hyperreals
-
-
-
- HyperNat Ultrapower construction of the hypernaturals
-
- HyperPow Powers theory for the hyperreals
-
- IntFloor Floor and Ceiling functions relating the reals and integers
-
- Integration Gage integrals
-
- Lim Theory of limits, continuous functions, and derivatives
-
-
- Log Logarithms for the reals
-
-
- MacLaurin MacLaurin series
-
-
- NatStar Star-transforms for the hypernaturals, to form non-standard extensions of sets and functions involving the naturals or reals
-
- NthRoot Existence of n-th roots of real numbers
-
- NSA Theory defining sets of infinite numbers, infinitesimals, the infinitely close relation, and their various algebraic properties.
-
- Poly Univariate real polynomials
-
- SEQ Convergence of sequences and series using standard and nonstandard analysis
-
- Series Finite summation and infinite series for the reals
-
- Star Nonstandard extensions of real sets and real functions
-
- Transcendental Power series and transcendental functions
-
- Last modified on $Date$
-
-
-
-
-
-lcp@cl.cam.ac.uk
-
-
diff -r ffb4099c316f -r b82a837f6959 src/HOL/Real/README.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 @@
-
-
-
-
-
-
- HOL/Real/README
-
-
-
- Real: Dedekind Cut Construction of the Real Line
-
- - Lubs Definition of upper bounds, lubs and so on, to support completeness proofs.
-
- PReal The positive reals constructed using Dedekind cuts
-
-
- Rational The rational numbers constructed as equivalence classes of integers
-
-
- RComplete The reals are complete: they satisfy the supremum property. They also have the Archimedean property.
-
-
- RealDef The real numbers, their ordering properties, and embedding of the integers and the natural numbers
-
-
- RealPow Real numbers raised to natural number powers
-
-
- Last modified on $Date$
-
- lcp@cl.cam.ac.uk
-
-
-
\ No newline at end of file