diff -r 8c3190b173aa -r 062a782d7402 src/HOL/README.html --- a/src/HOL/README.html Thu Sep 30 16:16:56 1999 +0200 +++ b/src/HOL/README.html Thu Sep 30 20:49:06 1999 +0200 @@ -47,7 +47,7 @@
a simple theory of Input/Output Automata
Isar_examples -
some Isabelle/Isar proof documents +
several Isabelle/Isar example proof documents
Lambda
a proof of the Church-Rosser theorem for lambda-calculus @@ -63,6 +63,9 @@ non-standard analysis. Also includes the positive rationals. Used to build the image HOL-Real. +
Real/HahnBanach +
the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar). +
Subst
defines a theory of substitution and unification.