# HG changeset patch
# User paulson
# Date 859987535 -7200
# Node ID 6d6fd10a9fdc7dd7870f4e1a242ed5054b79aa9d
# Parent  acee08856cc9a105809790372fdc512a752586b7
Now a non-trivial theory so that require_thy can find it

diff -r acee08856cc9 -r 6d6fd10a9fdc src/ZF/Datatype.thy
--- 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
+
diff -r acee08856cc9 -r 6d6fd10a9fdc src/ZF/Inductive.thy
--- 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