src/ZF/ex/ROOT.ML
author lcp
Tue Feb 28 10:53:56 1995 +0100 (1995-02-28)
changeset 919 49271bd72c42
parent 589 31847a7504ec
child 960 358a19a91d52
permissions -rw-r--r--
No longer calls maketest; instead, the Makefile writes the file
test.
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
lcp@919
     6
Executes miscellaneous 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
lcp@919
    11
(writeln"Root file for ZF Set Theory examples";
lcp@919
    12
 proof_timing := true;
clasohm@0
    13
lcp@919
    14
 loadpath := [".", "ex"];
clasohm@125
    15
lcp@919
    16
 time_use     "ex/misc.ML";
lcp@919
    17
 time_use_thy "ex/Ramsey";
clasohm@0
    18
lcp@919
    19
 (*Integers & Binary integer arithmetic*)
lcp@919
    20
 time_use_thy "ex/Bin";
clasohm@0
    21
lcp@919
    22
 (** Datatypes **)
lcp@919
    23
 time_use_thy "ex/BT";		(*binary trees*)
lcp@919
    24
 time_use_thy "ex/Data";		(*Sample datatype*)
lcp@919
    25
 time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
lcp@919
    26
 time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
lcp@919
    27
 time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
lcp@919
    28
 time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
lcp@919
    29
 time_use_thy "ex/Enum";		(*Enormous enumeration type*)
clasohm@0
    30
lcp@919
    31
 (** Inductive definitions **)
lcp@919
    32
 time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
lcp@919
    33
 time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
lcp@919
    34
 (*two Coq examples by Christine Paulin-Mohring*)
lcp@919
    35
 time_use_thy "ex/ListN";
lcp@919
    36
 time_use_thy "ex/Acc";
lcp@919
    37
 time_use_thy "ex/Comb";		(*Combinatory Logic example*)
lcp@919
    38
 time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
clasohm@0
    39
lcp@919
    40
 (** CoDatatypes **)
lcp@919
    41
 time_use_thy "ex/LList";
lcp@919
    42
 time_use_thy "ex/CoUnit";
clasohm@0
    43
lcp@919
    44
 writeln"END: Root file for ZF Set Theory examples"
lcp@919
    45
)  handle _ => exit 1;