Real/HahnBanach;
authorwenzelm
Thu Sep 30 20:49:06 1999 +0200 (1999-09-30)
changeset 7662062a782d7402
parent 7661 8c3190b173aa
child 7663 460fedf14b09
Real/HahnBanach;
src/HOL/README.html
     1.1 --- a/src/HOL/README.html	Thu Sep 30 16:16:56 1999 +0200
     1.2 +++ b/src/HOL/README.html	Thu Sep 30 20:49:06 1999 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  <DD>a simple theory of Input/Output Automata
     1.5  
     1.6  <DT>Isar_examples
     1.7 -<DD>some Isabelle/Isar proof documents
     1.8 +<DD>several Isabelle/Isar example proof documents
     1.9  
    1.10  <DT>Lambda
    1.11  <DD>a proof of the Church-Rosser theorem for lambda-calculus
    1.12 @@ -63,6 +63,9 @@
    1.13  non-standard analysis.  Also includes the positive rationals.  Used to build
    1.14  the image HOL-Real.
    1.15  
    1.16 +<DT>Real/HahnBanach
    1.17 +<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
    1.18 +
    1.19  <DT>Subst
    1.20  <DD>defines a theory of substitution and unification.
    1.21