--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Datatype.thy	Tue Nov 16 14:24:21 1993 +0100
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+Datatype = "constructor" + "inductive" + "coinductive" + Univ + QUniv
+               (*this must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file