src/ZF/ex/ROOT.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6045 6a9dc67d48f5
child 9000 c20d58286a51
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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
lcp@960
     9
writeln"Root file for ZF Set Theory examples";
wenzelm@4446
    10
set proof_timing;
clasohm@0
    11
clasohm@1351
    12
time_use     "misc.ML";
paulson@2248
    13
time_use_thy "Primes";          (*GCD theory*)
paulson@2248
    14
time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
paulson@2248
    15
time_use_thy "Limit";           (*Inverse limit construction of domains*)
paulson@5533
    16
time_use     "BinEx";		(*Binary integer arithmetic*)
clasohm@0
    17
lcp@960
    18
(** Datatypes **)
clasohm@1461
    19
time_use_thy "BT";              (*binary trees*)
clasohm@1461
    20
time_use_thy "Data";            (*Sample datatype*)
clasohm@1461
    21
time_use_thy "Term";            (*terms: recursion over the list functor*)
clasohm@1461
    22
time_use_thy "TF";              (*trees/forests: mutual recursion*)
clasohm@1461
    23
time_use_thy "Ntree";           (*variable-branching trees; function demo*)
clasohm@1461
    24
time_use_thy "Brouwer";         (*Infinite-branching trees*)
clasohm@1461
    25
time_use_thy "Enum";            (*Enormous enumeration type*)
clasohm@0
    26
lcp@960
    27
(** Inductive definitions **)
clasohm@1461
    28
time_use_thy "Rmap";            (*mapping a relation over a list*)
paulson@6045
    29
time_use_thy "Mutil";           (*mutilated chess board*)
clasohm@1461
    30
time_use_thy "PropLog";         (*completeness of propositional logic*)
lcp@960
    31
(*two Coq examples by Christine Paulin-Mohring*)
clasohm@1351
    32
time_use_thy "ListN";
clasohm@1351
    33
time_use_thy "Acc";
clasohm@1461
    34
time_use_thy "Comb";            (*Combinatory Logic example*)
clasohm@1461
    35
time_use_thy "Primrec";         (*Primitive recursive functions*)
clasohm@0
    36
lcp@960
    37
(** CoDatatypes **)
clasohm@1351
    38
time_use_thy "LList";
clasohm@1351
    39
time_use_thy "CoUnit";
clasohm@1296
    40
lcp@960
    41
writeln"END: Root file for ZF Set Theory examples";