--- a/src/ZF/Datatype.thy Wed Apr 02 15:24:42 1997 +0200
+++ b/src/ZF/Datatype.thy Wed Apr 02 15:25:35 1997 +0200
@@ -1,5 +1,14 @@
-(*Dummy theory to document dependencies *)
+(* Title: ZF/Datatype
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations
-Datatype = "constructor" + Inductive + Univ + QUniv
+ "Datatype" must be capital to avoid conflicts with ML's "datatype"
+*)
-(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
+Datatype = "constructor" + Inductive + Univ + QUniv +
+
+end
+