src/ZF/ex/ROOT.ML
author paulson
Wed Nov 27 13:01:07 1996 +0100 (1996-11-27)
changeset 2248 187d001fbe79
parent 1793 09fff2f0d727
child 4446 097004a470fb
permissions -rw-r--r--
Better indentation
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";
lcp@960
    12
proof_timing := true;
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*)
clasohm@0
    18
lcp@960
    19
(*Integers & Binary integer arithmetic*)
clasohm@1351
    20
time_use_thy "Bin";
clasohm@0
    21
lcp@960
    22
(** Datatypes **)
clasohm@1461
    23
time_use_thy "BT";              (*binary trees*)
clasohm@1461
    24
time_use_thy "Data";            (*Sample datatype*)
clasohm@1461
    25
time_use_thy "Term";            (*terms: recursion over the list functor*)
clasohm@1461
    26
time_use_thy "TF";              (*trees/forests: mutual recursion*)
clasohm@1461
    27
time_use_thy "Ntree";           (*variable-branching trees; function demo*)
clasohm@1461
    28
time_use_thy "Brouwer";         (*Infinite-branching trees*)
clasohm@1461
    29
time_use_thy "Enum";            (*Enormous enumeration type*)
clasohm@0
    30
lcp@960
    31
(** Inductive definitions **)
clasohm@1461
    32
time_use_thy "Rmap";            (*mapping a relation over a list*)
paulson@1613
    33
time_use_thy "Mutil";           (*mutilated checkerboard*)
clasohm@1461
    34
time_use_thy "PropLog";         (*completeness of propositional logic*)
lcp@960
    35
(*two Coq examples by Christine Paulin-Mohring*)
clasohm@1351
    36
time_use_thy "ListN";
clasohm@1351
    37
time_use_thy "Acc";
clasohm@1461
    38
time_use_thy "Comb";            (*Combinatory Logic example*)
clasohm@1461
    39
time_use_thy "Primrec";         (*Primitive recursive functions*)
clasohm@0
    40
lcp@960
    41
(** CoDatatypes **)
clasohm@1351
    42
time_use_thy "LList";
clasohm@1351
    43
time_use_thy "CoUnit";
clasohm@1296
    44
lcp@960
    45
writeln"END: Root file for ZF Set Theory examples";