src/ZF/ex/ROOT.ML
author clasohm
Tue Nov 21 12:43:09 1995 +0100 (1995-11-21)
changeset 1351 4a960c012383
parent 1296 ae31bb7774a7
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
removed make_chart;
theories are now read from the current directory (because of use_dir)
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@960
    11
writeln"Root file for ZF Set Theory examples";
lcp@960
    12
proof_timing := true;
clasohm@0
    13
clasohm@1351
    14
time_use     "misc.ML";
clasohm@1351
    15
time_use_thy "Ramsey";
clasohm@1351
    16
time_use_thy "Limit";
clasohm@0
    17
lcp@960
    18
(*Integers & Binary integer arithmetic*)
clasohm@1351
    19
time_use_thy "Bin";
clasohm@0
    20
lcp@960
    21
(** Datatypes **)
clasohm@1351
    22
time_use_thy "BT";		(*binary trees*)
clasohm@1351
    23
time_use_thy "Data";		(*Sample datatype*)
clasohm@1351
    24
time_use_thy "Term";		(*terms: recursion over the list functor*)
clasohm@1351
    25
time_use_thy "TF";		(*trees/forests: mutual recursion*)
clasohm@1351
    26
time_use_thy "Ntree";		(*variable-branching trees; function demo*)
clasohm@1351
    27
time_use_thy "Brouwer";		(*Infinite-branching trees*)
clasohm@1351
    28
time_use_thy "Enum";		(*Enormous enumeration type*)
clasohm@0
    29
lcp@960
    30
(** Inductive definitions **)
clasohm@1351
    31
time_use_thy "Rmap";		(*mapping a relation over a list*)
clasohm@1351
    32
time_use_thy "PropLog";		(*completeness of propositional logic*)
lcp@960
    33
(*two Coq examples by Christine Paulin-Mohring*)
clasohm@1351
    34
time_use_thy "ListN";
clasohm@1351
    35
time_use_thy "Acc";
clasohm@1351
    36
time_use_thy "Comb";		(*Combinatory Logic example*)
clasohm@1351
    37
time_use_thy "Primrec";		(*Primitive recursive functions*)
clasohm@0
    38
lcp@960
    39
(** CoDatatypes **)
clasohm@1351
    40
time_use_thy "LList";
clasohm@1351
    41
time_use_thy "CoUnit";
clasohm@1296
    42
lcp@960
    43
writeln"END: Root file for ZF Set Theory examples";