# HG changeset patch # User paulson # Date 1082375375 -7200 # Node ID ec1e67f88f4970cf9adeec457eeccffbe35ac0c4 # Parent 4a9cc3080dbcc37e0ff8e26e97ed7661661cd653 badly-needed updates diff -r 4a9cc3080dbc -r ec1e67f88f49 src/HOL/Complex/README.html --- 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 @@ -HOL/Complex/README +HOL/Complex/README + + -

Complex--The Complex Numbers

- -

This directory defines the type complex of the complex numbers, +

Complex: The Complex Numbers

This directory defines the type complex of the complex numbers, 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. + -

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 +

Last modified $Date$ diff -r 4a9cc3080dbc -r ec1e67f88f49 src/HOL/Hyperreal/README.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 @@ -HOL/Real/README + + HOL/Hyperreal/README + + -

Hyperreal--Ultrafilter Construction of the Non-Standard Reals

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. -

Zorn -Zorn's Lemma: proof based on the ZF version. -
Filter +
- Filter Theory of Filters and Ultrafilters. Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma. -
- HyperDef + +
- 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 -
- NSA -Theory defining sets of infinite numbers, infinitesimals, -the infinitely close relation, and their various algebraic properties. - -
- HyperNat -Ultrapower construction of the hypernaturals - -
- HyperPow -Powers theory for the hyperreals - -
- Star -Nonstandard extensions of real sets and real functions -
- NatStar -Nonstandard extensions of sets of naturals and functions on the natural -numbers - -
- SEQ -Theory of sequences developed using standard and nonstandard analysis +
- 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$ -
Lim -Theory of limits, continuous functions, and derivatives -
Series -Standard theory of finite summation and infinite series - -

- -

Last modified on $Date$ - -

lcp@cl.cam.ac.uk diff -r 4a9cc3080dbc -r ec1e67f88f49 src/HOL/Real/README.html --- 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 @@ -HOL/Real/README - -

Real--Dedekind Cut Construction of the Real Line

PNat The positive integers (very much the same as Nat.thy!) -
PRat The positive rationals -
PReal The positive reals constructed using Dedekind cuts -
RealDef The real numbers -
RealOrd More real numbers theorems- ordering -properties -
RealInt Embedding of the integers in the reals -
RealBin Binary arithmetic for the reals + -
Lubs Definition of upper bounds, lubs and so on. - (Useful e.g. in Fleuriot's NSA theory) -
RComplete Proof of completeness of reals in form of the supremum - property. Also proofs that the reals have the Archimedean - property. -
RealAbs The absolute value function defined for the reals -

- -

Hyperreal--Ultrapower Construction of the Non-Standard Reals

+ + + HOL/Real/README + -

-See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real -Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. -

- -

Zorn -Zorn's Lemma: proof based on the ZF version - -
Filter -Theory of Filters and Ultrafilters. -Main result is a version of the Ultrafilter Theorem proved using -Zorn's Lemma. - -
HyperDef -Ultrapower construction of the hyperreals + +
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 -
- HyperOrd -More hyperreal numbers theorems- ordering properties - -
- HRealAbs The absolute value function -defined for the hyperreals - - -
- NSA -Theory defining sets of infinite numbers, infinitesimals, -the infinitely close relation, and their various algebraic properties. - -
- HyperNat -Ultrapower construction of the hypernaturals - -
- HyperPow -Powers theory for the hyperreals - -
- Star -Nonstandard extensions of real sets and real functions +
- 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. -
- NatStar -Nonstandard extensions of sets of naturals and functions on the natural -numbers - -
- SEQ -Theory of sequences developed using standard and nonstandard analysis - -
- Lim -Theory of limits, continuous functions, and derivatives - -
- Series -Standard theory of finite summation and infinite series +
- 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
+ - - -

- -