src/ZF/Datatype.thy

--- a/src/ZF/Datatype.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Datatype.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,9 +3,10 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 
-(Co)Datatype Definitions for Zermelo-Fraenkel Set Theory.
 *)
 
+header{*Datatype and CoDatatype Definitions*}
+
 theory Datatype = Inductive + Univ + QUniv
   files
     "Tools/datatype_package.ML"