diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Datatype_Universe.thy --- a/src/HOL/Datatype_Universe.thy Thu Oct 12 18:44:35 2000 +0200 +++ b/src/HOL/Datatype_Universe.thy Fri Oct 13 08:28:21 2000 +0200 @@ -9,7 +9,7 @@ Could <*> be generalized to a general summation (Sigma)? *) -Datatype_Universe = Arithmetic + Sum_Type + +Datatype_Universe = NatArith + Sum_Type + (** lists, trees will be sets of nodes **)