HOL/Real/README

# HG changeset patch # User paulson # Date 978271947 -3600 # Node ID 0fb476ff855c9ea8977cf3ed3f7ff01da0fbb611 # Parent 9bc30e51144ceb83748cdc0892b1858ad62a8896 separation of HOL-Hyperreal from HOL-Real diff -r 9bc30e51144c -r 0fb476ff855c src/HOL/Hyperreal/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hyperreal/README.html Sun Dec 31 15:12:27 2000 +0100 @@ -0,0 +1,59 @@ + +HOL/Real/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. +

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

HOL/Real/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. -