src/ZF/InfDatatype.thy

--- a/src/ZF/InfDatatype.thy	Sun Jul 14 15:11:21 2002 +0200
+++ b/src/ZF/InfDatatype.thy	Sun Jul 14 15:14:43 2002 +0200
@@ -3,9 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Infinite-branching datatype definitions
 *)
 
+header{*Infinite-Branching Datatype Definitions*}
+
 theory InfDatatype = Datatype + Univ + Finite + Cardinal_AC:
 
 lemmas fun_Limit_VfromE =