src/ZF/ex/ROOT.ML
changeset 12192 6ef4ad110e90
parent 12088 6f463d16cbd0
child 12200 b544785b6cc9
equal deleted inserted replaced
12191:2c383ee7ff16 12192:6ef4ad110e90
     1 (*  Title:      ZF/ex/ROOT
     1 (*  Title:      ZF/ex/ROOT.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
     6 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory.
     7 *)
     7 *)
     8 
     8 
     9 time_use_thy "misc";
     9 time_use_thy "misc";
    10 time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
    10 time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
    11 time_use_thy "Primes";          (*GCD theory*)
    11 time_use_thy "Primes";          (*GCD theory*)
    13 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
    13 time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
    14 time_use_thy "Limit";           (*Inverse limit construction of domains*)
    14 time_use_thy "Limit";           (*Inverse limit construction of domains*)
    15 time_use_thy "BinEx";		(*Binary integer arithmetic*)
    15 time_use_thy "BinEx";		(*Binary integer arithmetic*)
    16 
    16 
    17 (** Datatypes **)
    17 (** Datatypes **)
    18 time_use_thy "BT";              (*binary trees*)
       
    19 time_use_thy "Data";            (*Sample datatype*)
       
    20 time_use_thy "Term";            (*terms: recursion over the list functor*)
    18 time_use_thy "Term";            (*terms: recursion over the list functor*)
    21 time_use_thy "TF";              (*trees/forests: mutual recursion*)
    19 time_use_thy "TF";              (*trees/forests: mutual recursion*)
    22 time_use_thy "Ntree";           (*variable-branching trees; function demo*)
    20 time_use_thy "Ntree";           (*variable-branching trees; function demo*)
    23 time_use_thy "Brouwer";         (*Infinite-branching trees*)
    21 time_use_thy "Brouwer";         (*Infinite-branching trees*)
    24 time_use_thy "Enum";            (*Enormous enumeration type*)
       
    25 
    22 
    26 (** CoDatatypes **)
    23 (** CoDatatypes **)
    27 time_use_thy "LList";
    24 time_use_thy "LList";
    28 time_use_thy "CoUnit";
    25 time_use_thy "CoUnit";