--- a/src/HOL/Real/PReal.thy Thu Sep 15 22:16:23 2005 +0200 +++ b/src/HOL/Real/PReal.thy Thu Sep 15 23:16:04 2005 +0200 @@ -7,6 +7,8 @@ provides some of the definitions. *) +header {* Positive real numbers *} + theory PReal imports Rational begin