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