src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Thu Nov 10 21:14:05 2005 +0100
+++ b/src/HOL/Fun.thy	Fri Nov 11 00:09:37 2005 +0100
@@ -2,9 +2,9 @@
     ID:         $Id$
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
+*)
 
-Notions about functions.
-*)
+header {* Notions about functions *}
 
 theory Fun
 imports Typedef