src/ZF/ex/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 6349 f7750d816c21
child 9647 e9623f47275b
permissions -rw-r--r--
cleaned up;
clasohm@1461
     1
(*  Title:      ZF/ex/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
lcp@919
     6
Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
clasohm@0
     7
*)
clasohm@0
     8
clasohm@1351
     9
time_use     "misc.ML";
paulson@2248
    10
time_use_thy "Primes";          (*GCD theory*)
paulson@2248
    11
time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
paulson@2248
    12
time_use_thy "Limit";           (*Inverse limit construction of domains*)
paulson@5533
    13
time_use     "BinEx";		(*Binary integer arithmetic*)
clasohm@0
    14
lcp@960
    15
(** Datatypes **)
clasohm@1461
    16
time_use_thy "BT";              (*binary trees*)
clasohm@1461
    17
time_use_thy "Data";            (*Sample datatype*)
clasohm@1461
    18
time_use_thy "Term";            (*terms: recursion over the list functor*)
clasohm@1461
    19
time_use_thy "TF";              (*trees/forests: mutual recursion*)
clasohm@1461
    20
time_use_thy "Ntree";           (*variable-branching trees; function demo*)
clasohm@1461
    21
time_use_thy "Brouwer";         (*Infinite-branching trees*)
clasohm@1461
    22
time_use_thy "Enum";            (*Enormous enumeration type*)
clasohm@0
    23
lcp@960
    24
(** Inductive definitions **)
clasohm@1461
    25
time_use_thy "Rmap";            (*mapping a relation over a list*)
paulson@6045
    26
time_use_thy "Mutil";           (*mutilated chess board*)
clasohm@1461
    27
time_use_thy "PropLog";         (*completeness of propositional logic*)
lcp@960
    28
(*two Coq examples by Christine Paulin-Mohring*)
clasohm@1351
    29
time_use_thy "ListN";
clasohm@1351
    30
time_use_thy "Acc";
clasohm@1461
    31
time_use_thy "Comb";            (*Combinatory Logic example*)
clasohm@1461
    32
time_use_thy "Primrec";         (*Primitive recursive functions*)
clasohm@0
    33
lcp@960
    34
(** CoDatatypes **)
clasohm@1351
    35
time_use_thy "LList";
clasohm@1351
    36
time_use_thy "CoUnit";