src/ZF/ex/ROOT.ML
author clasohm
Wed Oct 06 14:45:04 1993 +0100 (1993-10-06)
changeset 34 747f1aad03cf
parent 16 0b033d50ca1c
child 56 2caa6f49f06e
permissions -rw-r--r--
changed filenames to lower case name of theory the file contains
(only one theory per file, therefore llist.ML has been split)
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@0
    14
time_use     "ex/misc.ML";
clasohm@0
    15
time_use_thy "ex/ramsey";
clasohm@0
    16
clasohm@0
    17
(*Equivalence classes and integers*)
clasohm@0
    18
time_use_thy "ex/equiv";
clasohm@0
    19
time_use_thy "ex/integ";
clasohm@0
    20
(*Binary integer arithmetic*)
clasohm@0
    21
use          "ex/twos-compl.ML";
clasohm@0
    22
time_use     "ex/bin.ML";
clasohm@34
    23
time_use_thy "ex/binfn";
clasohm@0
    24
clasohm@0
    25
(** Datatypes **)
clasohm@0
    26
(*binary trees*)
clasohm@0
    27
time_use     "ex/bt.ML";
clasohm@34
    28
time_use_thy "ex/bt_fn";
clasohm@0
    29
(*terms: recursion over the list functor*)
clasohm@0
    30
time_use     "ex/term.ML";
clasohm@34
    31
time_use_thy "ex/termfn";
clasohm@0
    32
(*trees/forests: mutual recursion*)
clasohm@0
    33
time_use     "ex/tf.ML";
clasohm@34
    34
time_use_thy "ex/tf_fn";
clasohm@0
    35
(*Enormous enumeration type -- could be even bigger?*)
clasohm@0
    36
time_use     "ex/enum.ML";
clasohm@0
    37
clasohm@0
    38
(** Inductive definitions **)
lcp@16
    39
(*mapping a relation over a list*)
lcp@16
    40
time_use     "ex/rmap.ML";
clasohm@0
    41
(*completeness of propositional logic*)
clasohm@0
    42
time_use     "ex/prop.ML";
clasohm@34
    43
time_use_thy "ex/propthms";
clasohm@0
    44
(*two Coq examples by Ch. Paulin-Mohring*)
clasohm@0
    45
time_use     "ex/listn.ML";
clasohm@0
    46
time_use     "ex/acc.ML";
clasohm@0
    47
(*Diamond property for combinatory logic*)
clasohm@0
    48
time_use     "ex/comb.ML";
clasohm@0
    49
time_use_thy "ex/contract";
clasohm@0
    50
time_use     "ex/parcontract.ML";
lcp@16
    51
time_use_thy "ex/primrec";
clasohm@0
    52
clasohm@0
    53
(** Co-Datatypes **)
clasohm@0
    54
time_use     "ex/llist.ML";
clasohm@34
    55
time_use     "ex/llist_eq.ML";
clasohm@34
    56
time_use_thy "ex/llistfn";
clasohm@0
    57
clasohm@0
    58
clasohm@0
    59
maketest"END: Root file for ZF Set Theory examples";