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