# HG changeset patch
# User huffman
# Date 1126818964 -7200
# Node ID 8a2de150b5f1846ab897792ecf59080f3c6da8b5
# Parent  3c45d890d47c9d2ec4645e940adfcb29d945cf64
add header

diff -r 3c45d890d47c -r 8a2de150b5f1 src/HOL/Real/PReal.thy
--- 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