src/ZF/Datatype.thy
changeset 578 efc648d29dd0
parent 516 1957113f0d7d
child 809 1daa0269eb5d
--- a/src/ZF/Datatype.thy	Thu Aug 25 10:41:17 1994 +0200
+++ b/src/ZF/Datatype.thy	Thu Aug 25 12:09:21 1994 +0200
@@ -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