src/ZF/ex/ROOT.ML
author lcp
Wed Jul 27 16:03:16 1994 +0200 (1994-07-27)
changeset 489 0449a7f1add3
parent 365 796c5e305b31
child 515 abcc438e7c27
permissions -rw-r--r--
Addition of infinite branching datatypes
clasohm@0
     1
(*  Title: 	ZF/ex/ROOT
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Executes all examples for Zermelo-Fraenkel Set Theory
clasohm@0
     7
*)
clasohm@0
     8
lcp@16
     9
ZF_build_completed;	(*Make examples fail if ZF did*)
clasohm@0
    10
clasohm@0
    11
writeln"Root file for ZF Set Theory examples";
clasohm@0
    12
proof_timing := true;
clasohm@0
    13
clasohm@125
    14
loadpath := [".", "ex"];
clasohm@125
    15
clasohm@0
    16
time_use     "ex/misc.ML";
clasohm@125
    17
time_use_thy "ex/Ramsey";
clasohm@0
    18
clasohm@0
    19
(*Equivalence classes and integers*)
clasohm@125
    20
time_use_thy "ex/Equiv";
clasohm@125
    21
time_use_thy "ex/Integ";
clasohm@0
    22
(*Binary integer arithmetic*)
clasohm@91
    23
use          "ex/twos_compl.ML";
clasohm@125
    24
time_use_thy "ex/BinFn";
clasohm@0
    25
clasohm@0
    26
(** Datatypes **)
lcp@180
    27
time_use_thy "ex/BT_Fn";	(*binary trees*)
lcp@180
    28
time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
lcp@180
    29
time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
lcp@489
    30
time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
lcp@489
    31
time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
lcp@180
    32
time_use_thy "ex/Data";		(*Sample datatype*)
lcp@180
    33
time_use_thy "ex/Enum";		(*Enormous enumeration type*)
clasohm@0
    34
clasohm@0
    35
(** Inductive definitions **)
lcp@180
    36
time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
lcp@180
    37
time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
clasohm@0
    38
(*two Coq examples by Ch. Paulin-Mohring*)
lcp@180
    39
time_use_thy "ex/ListN";
lcp@180
    40
time_use_thy "ex/Acc";
lcp@180
    41
time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
lcp@180
    42
time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
clasohm@125
    43
time_use_thy "ex/Primrec0";
clasohm@0
    44
lcp@120
    45
(** CoDatatypes **)
clasohm@76
    46
time_use_thy "ex/LList";
clasohm@125
    47
time_use_thy "ex/LListFn";
lcp@365
    48
time_use     "ex/CoUnit.ML";
clasohm@0
    49
clasohm@0
    50
maketest"END: Root file for ZF Set Theory examples";