HOL/Real/README

# HG changeset patch # User wenzelm # Date 1006293230 -3600 # Node ID 78bc1f3462b584f657202fd46dddc3a822f3ec9a # Parent 1886dc96b7e963a027443dd50fec7d566aab1a68 fixed links etc.; diff -r 1886dc96b7e9 -r 78bc1f3462b5 src/HOL/GroupTheory/README.html --- a/src/HOL/GroupTheory/README.html Tue Nov 20 22:53:05 2001 +0100 +++ b/src/HOL/GroupTheory/README.html Tue Nov 20 22:53:50 2001 +0100 @@ -12,29 +12,29 @@ Here is an outline of the directory's contents:

Theory Bij +
Theory Bij defines bijections over sets and operations on them and shows that they are a group. -
Theory DirProd +
Theory DirProd defines the product of two groups and proves that it is a group again. -
Theory FactGroup +
Theory FactGroup defines the factorization of a group and shows that the factorization a normal subgroup is a group. -
Theory Homomorphism +
Theory Homomorphism defines homomorphims and automorphisms for groups and rings and shows that ring automorphisms are a group by using the previous result for bijections. -
Theory Ring -and RingConstr +
Theory Ring +and RingConstr defines rings, proves a few basic theorems and constructs a lambda function to extract the group that is part of the ring showing that it is an abelian group. -
Theory Sylow +
Theory Sylow contains a proof of the first Sylow theorem.

diff -r 1886dc96b7e9 -r 78bc1f3462b5 src/HOL/Hyperreal/README.html --- a/src/HOL/Hyperreal/README.html Tue Nov 20 22:53:05 2001 +0100 +++ b/src/HOL/Hyperreal/README.html Tue Nov 20 22:53:50 2001 +0100 @@ -2,9 +2,8 @@ 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 @@ -44,7 +43,6 @@
Series Standard theory of finite summation and infinite series -

Last modified on $Date$ diff -r 1886dc96b7e9 -r 78bc1f3462b5 src/HOL/Real/README.html --- a/src/HOL/Real/README.html Tue Nov 20 22:53:05 2001 +0100 +++ b/src/HOL/Real/README.html Tue Nov 20 22:53:50 2001 +0100 @@ -3,7 +3,7 @@

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 @@ -22,8 +22,11 @@

Hyperreal--Ultrapower 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. + +
+See J. D. Fleuriot and L. C. Paulson. Mechanizing Nonstandard Real +Analysis. LMS J. Computation and Mathematics 3 (2000), 140-190. +
- Zorn