# HG changeset patch
# User lcp
# Date 787847430 -3600
# Node ID 91c68f74f4585b7f2a6ec9ac97e23e2d8f5cd95e
# Parent  1daa0269eb5d46cbe2af165b247e414a9011cb98
removed quotes around "Datatype",
and removed needless mention of [Q]Univ

diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/IMP/Com.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -8,7 +8,7 @@
 And their Operational semantics
 *)
 
-Com = Univ + "Datatype" +
+Com = Datatype +
 
 (** Arithmetic expressions **)
 consts  loc  :: "i"
diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/List.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -10,7 +10,7 @@
 although complicating its derivation.
 *)
 
-List = "Datatype" + Univ + 
+List = Datatype + 
 
 consts
   "@"	     :: "[i,i]=>i"      			(infixr 60)
diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/CoUnit.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -10,7 +10,7 @@
   Report 334,  Cambridge University Computer Laboratory.  1994.
 *)
 
-CoUnit = QUniv + "Datatype" +
+CoUnit = Datatype +
 
 (*This degenerate definition does not work well because the one constructor's
   definition is trivial!  The same thing occurs with Aczel's Special Final
diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/Comb.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Univ + "Datatype" +
+Comb = Datatype +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 consts comb :: "i"
diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/ex/Enum.thy
--- a/src/ZF/ex/Enum.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/Enum.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -8,7 +8,7 @@
 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
-Enum = Univ + "Datatype" + 
+Enum = Datatype + 
 
 consts
   enum :: "i"
diff -r 1daa0269eb5d -r 91c68f74f458 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/LList.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -14,7 +14,7 @@
 a typing rule for it, based on some notion of "productivity..."
 *)
 
-LList = QUniv + "Datatype" +
+LList = Datatype +
 
 consts
   llist  :: "i=>i"