src/ZF/ex/ROOT.ML
author lcp
Wed Jul 27 16:03:16 1994 +0200 (1994-07-27)
changeset 489 0449a7f1add3
parent 365 796c5e305b31
child 515 abcc438e7c27
permissions -rw-r--r--
Addition of infinite branching datatypes
     1 (*  Title: 	ZF/ex/ROOT
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Executes all examples for Zermelo-Fraenkel Set Theory
     7 *)
     8 
     9 ZF_build_completed;	(*Make examples fail if ZF did*)
    10 
    11 writeln"Root file for ZF Set Theory examples";
    12 proof_timing := true;
    13 
    14 loadpath := [".", "ex"];
    15 
    16 time_use     "ex/misc.ML";
    17 time_use_thy "ex/Ramsey";
    18 
    19 (*Equivalence classes and integers*)
    20 time_use_thy "ex/Equiv";
    21 time_use_thy "ex/Integ";
    22 (*Binary integer arithmetic*)
    23 use          "ex/twos_compl.ML";
    24 time_use_thy "ex/BinFn";
    25 
    26 (** Datatypes **)
    27 time_use_thy "ex/BT_Fn";	(*binary trees*)
    28 time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
    29 time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
    30 time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
    31 time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
    32 time_use_thy "ex/Data";		(*Sample datatype*)
    33 time_use_thy "ex/Enum";		(*Enormous enumeration type*)
    34 
    35 (** Inductive definitions **)
    36 time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
    37 time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
    38 (*two Coq examples by Ch. Paulin-Mohring*)
    39 time_use_thy "ex/ListN";
    40 time_use_thy "ex/Acc";
    41 time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
    42 time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
    43 time_use_thy "ex/Primrec0";
    44 
    45 (** CoDatatypes **)
    46 time_use_thy "ex/LList";
    47 time_use_thy "ex/LListFn";
    48 time_use     "ex/CoUnit.ML";
    49 
    50 maketest"END: Root file for ZF Set Theory examples";