src/ZF/ex/ROOT.ML
changeset 489 0449a7f1add3
parent 365 796c5e305b31
child 515 abcc438e7c27
     1.1 --- a/src/ZF/ex/ROOT.ML	Wed Jul 27 15:33:42 1994 +0200
     1.2 +++ b/src/ZF/ex/ROOT.ML	Wed Jul 27 16:03:16 1994 +0200
     1.3 @@ -27,6 +27,8 @@
     1.4  time_use_thy "ex/BT_Fn";	(*binary trees*)
     1.5  time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
     1.6  time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
     1.7 +time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
     1.8 +time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
     1.9  time_use_thy "ex/Data";		(*Sample datatype*)
    1.10  time_use_thy "ex/Enum";		(*Enormous enumeration type*)
    1.11