isabelle: src/HOL/Real/Hyperreal/README.html@50be659d4222 (annotated)

5979 11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	1	<!-- $Id$ -->
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	2	<HTML><HEAD><TITLE>HOL/Real/README</TITLE></HEAD><BODY>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	3
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	4	<H2>Hyperreal--Ultrafilter Construction of the Non-Standard Reals</H2>
10055 2264bdd8becc * empty log message * fleuriot parents: 10043 diff changeset	5	<LI> See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard
2264bdd8becc * empty log message * fleuriot parents: 10043 diff changeset	6	Real Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190.
2264bdd8becc * empty log message * fleuriot parents: 10043 diff changeset	7	<UL>
5979 11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	8
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	9	<UL>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	10	<LI><A HREF="Zorn.html">Zorn</A>
5981 ec5c3d17969f fixed a link paulson parents: 5979 diff changeset	11	Zorn's Lemma: proof based on the <A HREF="../../../ZF/Zorn.html">ZF version</A>
5979 11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	12
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	13	<LI><A HREF="Filter.html">Filter</A>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	14	Theory of Filters and Ultrafilters.
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	15	Main result is a version of the Ultrafilter Theorem proved using
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	16	Zorn's Lemma.
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	17
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	18	<LI><A HREF="HyperDef.html">HyperDef</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	19	Ultrapower construction of the hyperreals
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	20
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	21	<LI><A HREF="NSA.html">NSA</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	22	Theory defining sets of infinite numbers, infinitesimals,
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	23	the infinitely close relation, and their various algebraic properties.
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	24
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	25	<LI><A HREF="HyperNat.html">HyperNat</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	26	Ultrapower construction of the hypernaturals
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	27
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	28	<LI><A HREF="HyperPow.html">HyperPow</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	29	Powers theory for the hyperreals
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	30
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	31	<LI><A HREF="Star.html">Star</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	32	Nonstandard extensions of real sets and real functions
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	33
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	34	<LI><A HREF="NatStar.html">NatStar</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	35	Nonstandard extensions of sets of naturals and functions on the natural
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	36	numbers
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	37
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	38	<LI><A HREF="SEQ.html">SEQ</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	39	Theory of sequences developed using standard and nonstandard analysis
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	40
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	41	<LI><A HREF="Lim.html">Lim</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	42	Theory of limits, continuous functions, and derivatives
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	43
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	44	<LI><A HREF="Series.html">Series</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	45	Standard theory of finite summation and infinite series
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	46
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	47
5979 11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	48	</UL>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	49
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	50	<P>Last modified on $Date$
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	51
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	52	<HR>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	53
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	54	<ADDRESS>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	55	<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	56	</ADDRESS>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	57	</BODY></HTML>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	58
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	59

author	wenzelm
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 10055	2264bdd8becc
permissions	-rw-r--r--