# HG changeset patch
# User lcp
# Date 794579868 -3600
# Node ID a94ef3eed456d3a0611fc2ddca1d799ba42a2b09
# Parent  2e0203309287293f346b8294a0a1389968ed013b
Changed Univ to Datatype in parents

diff -r 2e0203309287 -r a94ef3eed456 src/ZF/ex/BT.thy
--- 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"
diff -r 2e0203309287 -r a94ef3eed456 src/ZF/ex/Bin.thy
--- 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"
diff -r 2e0203309287 -r a94ef3eed456 src/ZF/ex/Data.thy
--- 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"
diff -r 2e0203309287 -r a94ef3eed456 src/ZF/ex/PropLog.thy
--- 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