src/ZF/Datatype.thy
changeset 809 1daa0269eb5d
parent 578 efc648d29dd0
child 2870 6d6fd10a9fdc
--- a/src/ZF/Datatype.thy	Mon Dec 19 15:17:29 1994 +0100
+++ b/src/ZF/Datatype.thy	Mon Dec 19 15:22:42 1994 +0100
@@ -1,5 +1,5 @@
 (*Dummy theory to document dependencies *)
 
-Datatype = "constructor" + "Inductive" + Univ + QUniv
+Datatype = "constructor" + Inductive + Univ + QUniv
 
-(*Datatype must be capital to avoid conflicts with ML's "datatype" *)
\ No newline at end of file
+(*Datatype must be capital to avoid conflicts with ML's "datatype" *)