--- a/src/ZF/ex/BT.thy Tue Mar 07 13:34:33 1995 +0100
+++ b/src/ZF/ex/BT.thy Tue Mar 07 13:37:48 1995 +0100
@@ -6,7 +6,7 @@
Binary trees
*)
-BT = Univ +
+BT = Datatype +
consts
bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i"
n_nodes :: "i=>i"
--- a/src/ZF/ex/Bin.thy Tue Mar 07 13:34:33 1995 +0100
+++ b/src/ZF/ex/Bin.thy Tue Mar 07 13:37:48 1995 +0100
@@ -18,7 +18,7 @@
Division is not defined yet!
*)
-Bin = Integ + Univ + "twos_compl" +
+Bin = Integ + Datatype + "twos_compl" +
consts
bin_rec :: "[i, i, i, [i,i,i]=>i] => i"
--- a/src/ZF/ex/Data.thy Tue Mar 07 13:34:33 1995 +0100
+++ b/src/ZF/ex/Data.thy Tue Mar 07 13:37:48 1995 +0100
@@ -7,7 +7,7 @@
It has four contructors, of arities 0-3, and two parameters A and B.
*)
-Data = Univ +
+Data = Datatype +
consts
data :: "[i,i] => i"
--- a/src/ZF/ex/PropLog.thy Tue Mar 07 13:34:33 1995 +0100
+++ b/src/ZF/ex/PropLog.thy Tue Mar 07 13:37:48 1995 +0100
@@ -7,7 +7,7 @@
of the propositional tautologies.
*)
-PropLog = Finite + Univ +
+PropLog = Finite + Datatype +
(** The datatype of propositions; note mixfix syntax **)
consts