src/ZF/ex/ROOT.ML
author clasohm
Tue Nov 16 14:26:15 1993 +0100 (1993-11-16)
changeset 125 bba27d15d76e
parent 120 09287f26bfb8
child 180 8962c2b0dc2b
permissions -rw-r--r--
changed use_thy's parameter to exact theory name
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@0
    24
time_use     "ex/bin.ML";
clasohm@125
    25
time_use_thy "ex/BinFn";
clasohm@0
    26
clasohm@0
    27
(** Datatypes **)
clasohm@0
    28
(*binary trees*)
clasohm@0
    29
time_use     "ex/bt.ML";
clasohm@125
    30
time_use_thy "ex/BT_Fn";
clasohm@0
    31
(*terms: recursion over the list functor*)
clasohm@0
    32
time_use     "ex/term.ML";
clasohm@125
    33
time_use_thy "ex/TermFn";
clasohm@0
    34
(*trees/forests: mutual recursion*)
clasohm@0
    35
time_use     "ex/tf.ML";
clasohm@125
    36
time_use_thy "ex/TF_Fn";
lcp@56
    37
(*Sample datatype; enormous enumeration type*)
lcp@56
    38
time_use     "ex/data.ML";
clasohm@0
    39
time_use     "ex/enum.ML";
clasohm@0
    40
clasohm@0
    41
(** Inductive definitions **)
lcp@16
    42
(*mapping a relation over a list*)
lcp@16
    43
time_use     "ex/rmap.ML";
clasohm@0
    44
(*completeness of propositional logic*)
clasohm@0
    45
time_use     "ex/prop.ML";
clasohm@125
    46
time_use_thy "ex/PropLog";
clasohm@0
    47
(*two Coq examples by Ch. Paulin-Mohring*)
clasohm@0
    48
time_use     "ex/listn.ML";
clasohm@0
    49
time_use     "ex/acc.ML";
clasohm@0
    50
(*Diamond property for combinatory logic*)
clasohm@0
    51
time_use     "ex/comb.ML";
clasohm@125
    52
time_use_thy "ex/Contract0";
clasohm@0
    53
time_use     "ex/parcontract.ML";
clasohm@125
    54
time_use_thy "ex/Primrec0";
clasohm@0
    55
lcp@120
    56
(** CoDatatypes **)
clasohm@76
    57
time_use_thy "ex/LList";
clasohm@34
    58
time_use     "ex/llist_eq.ML";
clasohm@125
    59
time_use_thy "ex/LListFn";
lcp@95
    60
time_use     "ex/counit.ML";
clasohm@0
    61
clasohm@0
    62
maketest"END: Root file for ZF Set Theory examples";