isabelle: src/HOL/Real/Hyperreal/README.html@a0364652e115 (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>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	5
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	6	<UL>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	7	<LI><A HREF="Zorn.html">Zorn</A>
5981 ec5c3d17969f fixed a link paulson parents: 5979 diff changeset	8	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	9
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	10	<LI><A HREF="Filter.html">Filter</A>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	11	Theory of Filters and Ultrafilters.
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	12	Main result is a version of the Ultrafilter Theorem proved using
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	13	Zorn's Lemma.
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	14
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	15	<LI><A HREF="HyperDef.html">HyperDef</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	16	Ultrapower construction of the hyperreals
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="NSA.html">NSA</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	19	Theory defining sets of infinite numbers, infinitesimals,
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	20	the infinitely close relation, and their various algebraic properties.
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	21
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	22	<LI><A HREF="HyperNat.html">HyperNat</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	23	Ultrapower construction of the hypernaturals
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="HyperPow.html">HyperPow</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	26	Powers theory for the hyperreals
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="Star.html">Star</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	29	Nonstandard extensions of real sets and real functions
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="NatStar.html">NatStar</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	32	Nonstandard extensions of sets of naturals and functions on the natural
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	33	numbers
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	34
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	35	<LI><A HREF="SEQ.html">SEQ</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	36	Theory of sequences developed using standard and nonstandard analysis
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="Lim.html">Lim</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	39	Theory of limits, continuous functions, and derivatives
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="Series.html">Series</A>
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	42	Standard theory of finite summation and infinite series
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	43
a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	44
5979 11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	45	</UL>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	46
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	47	<P>Last modified on $Date$
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	48
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	49	<HR>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	50
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	51	<ADDRESS>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	52	<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	53	</ADDRESS>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	54	</BODY></HTML>
11cbf236ca16 Addition of Hyperreal theories Zorn and Filter paulson parents: diff changeset	55
10043 a0364652e115 Updated Files with new theorems fleuriot parents: 5981 diff changeset	56

author	fleuriot
	Thu, 21 Sep 2000 12:11:38 +0200
changeset 10043	a0364652e115
parent 5981	ec5c3d17969f
child 10055	2264bdd8becc
permissions	-rw-r--r--