Now a non-trivial theory so that require_thy can find it

--- 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
+

--- a/src/ZF/Inductive.thy	Wed Apr 02 15:24:42 1997 +0200
+++ b/src/ZF/Inductive.thy	Wed Apr 02 15:25:35 1997 +0200
@@ -1,3 +1,5 @@
 (*Dummy theory to document dependencies *)
 
-Inductive = Fixedpt + Sum + QPair + "indrule"
+Inductive = Fixedpt + Sum + QPair + "indrule" +
+
+end