| changeset 10214 | 77349ed89f45 |
| parent 10213 | 01c2744a3786 |
| child 10832 | e33b47e4246d |
--- 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 **)