--- 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"
--- 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)
--- 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
--- 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"
--- 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"
--- 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"