src/HOL/Real/RealPow.thy

--- a/src/HOL/Real/RealPow.thy	Wed Sep 20 00:24:24 2006 +0200
+++ b/src/HOL/Real/RealPow.thy	Wed Sep 20 07:42:12 2006 +0200
@@ -2,9 +2,9 @@
     ID          : $Id$
     Author      : Jacques D. Fleuriot  
     Copyright   : 1998  University of Cambridge
-    Description : Natural powers theory
+*)
 
-*)
+header {* Natural powers theory *}
 
 theory RealPow
 imports RealDef