src/ZF/Datatype.thy

--- a/src/ZF/Datatype.thy	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/Datatype.thy	Fri Aug 12 12:51:34 1994 +0200
@@ -1,4 +1,5 @@
 (*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
+Datatype = "constructor" + "inductive" + Univ + QUniv
+
+(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file