# HG changeset patch
# User paulson
# Date 1082546317 -7200
# Node ID ffb4099c316f94314d06c2dfbd61c5718805d756
# Parent 8553a957cffa73db48ff9fc56ef9b95742815bc4
fixed to include Real and Hyperreal
diff -r 8553a957cffa -r ffb4099c316f src/HOL/Complex/README.html
--- a/src/HOL/Complex/README.html Tue Apr 20 04:09:19 2004 +0200
+++ b/src/HOL/Complex/README.html Wed Apr 21 13:18:37 2004 +0200
@@ -7,19 +7,52 @@
with numeric constants and some complex analysis. The development includes
nonstandard analysis for the complex numbers. Note that the image
HOL-Complex includes theories from the directories
-HOL/Real and HOL/Hyperreal.
-
-
-
+HOL/Real and HOL/Hyperreal. They define other types including real (the real numbers) and hypreal (the hyperreal or non-standard reals).
- CLim Limits, continuous functions, and derivatives for the complex numbers
- CSeries Finite summation and infinite series for the complex numbers
- CStar Star-transforms for the complex numbers, to form non-standard extensions of sets and functions
- Complex The complex numbers
- NSCA Nonstandard complex analysis
- NSComplex Ultrapower construction of the nonstandard complex numbers
+
- NSInduct Nonstandard induction for the hypernatural numbers
+
+
+
+ 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
+
+ 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 $Date$
+
Last modified $Date$