# HG changeset patch
# User huffman
# Date 1158730932 -7200
# Node ID 45fe31e72391179dd48093547ed29660749ff702
# Parent  e98f59806244598114bcdca2791c1dd5eda619f9
add header

diff -r e98f59806244 -r 45fe31e72391 src/HOL/Real/Ferrante_Rackoff.thy
--- a/src/HOL/Real/Ferrante_Rackoff.thy	Wed Sep 20 00:24:24 2006 +0200
+++ b/src/HOL/Real/Ferrante_Rackoff.thy	Wed Sep 20 07:42:12 2006 +0200
@@ -1,9 +1,9 @@
 (*
     ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
+*)
 
-Ferrante and Rackoff Algorithm: LCF-proof-synthesis version.
-*)
+header {* Ferrante and Rackoff Algorithm: LCF-proof-synthesis version. *}
 
 theory Ferrante_Rackoff
 imports RealPow
diff -r e98f59806244 -r 45fe31e72391 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