src/ZF/ex/ROOT.ML
author lcp
Wed Aug 17 10:38:37 1994 +0200 (1994-08-17)
changeset 540 e30c23731c2d
parent 526 85d7ff169b9c
child 589 31847a7504ec
permissions -rw-r--r--
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
Should be able to delete this after fixing the treatment of orphans.
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
lcp@540
    19
(*Integers & Binary integer arithmetic*)
lcp@540
    20
use "ex/twos_compl.ML";		(*can delete after autoloader change
lcp@540
    21
				  and addition of "twos_compl" to Bin.thy*)
lcp@515
    22
time_use_thy "ex/Bin";
clasohm@0
    23
clasohm@0
    24
(** Datatypes **)
lcp@515
    25
time_use_thy "ex/BT";		(*binary trees*)
lcp@526
    26
time_use_thy "ex/Data";		(*Sample datatype*)
lcp@515
    27
time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
lcp@515
    28
time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
lcp@489
    29
time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
lcp@526
    30
time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
lcp@180
    31
time_use_thy "ex/Enum";		(*Enormous enumeration type*)
clasohm@0
    32
clasohm@0
    33
(** Inductive definitions **)
lcp@180
    34
time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
lcp@180
    35
time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
lcp@515
    36
(*two Coq examples by Christine Paulin-Mohring*)
lcp@180
    37
time_use_thy "ex/ListN";
lcp@180
    38
time_use_thy "ex/Acc";
lcp@515
    39
time_use_thy "ex/Comb";		(*Combinatory Logic example*)
lcp@526
    40
time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
clasohm@0
    41
lcp@120
    42
(** CoDatatypes **)
clasohm@76
    43
time_use_thy "ex/LList";
lcp@526
    44
time_use_thy "ex/CoUnit";
clasohm@0
    45
clasohm@0
    46
maketest"END: Root file for ZF Set Theory examples";