src/ZF/ex/ROOT.ML
author lcp
Mon Nov 15 14:41:25 1993 +0100 (1993-11-15)
changeset 120 09287f26bfb8
parent 95 2246a80b1cb5
child 125 bba27d15d76e
permissions -rw-r--r--
changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs
     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 time_use     "ex/misc.ML";
    15 time_use_thy "ex/ramsey";
    16 
    17 (*Equivalence classes and integers*)
    18 time_use_thy "ex/equiv";
    19 time_use_thy "ex/integ";
    20 (*Binary integer arithmetic*)
    21 use          "ex/twos_compl.ML";
    22 time_use     "ex/bin.ML";
    23 time_use_thy "ex/binfn";
    24 
    25 (** Datatypes **)
    26 (*binary trees*)
    27 time_use     "ex/bt.ML";
    28 time_use_thy "ex/bt_fn";
    29 (*terms: recursion over the list functor*)
    30 time_use     "ex/term.ML";
    31 time_use_thy "ex/termfn";
    32 (*trees/forests: mutual recursion*)
    33 time_use     "ex/tf.ML";
    34 time_use_thy "ex/tf_fn";
    35 (*Sample datatype; enormous enumeration type*)
    36 time_use     "ex/data.ML";
    37 time_use     "ex/enum.ML";
    38 
    39 (** Inductive definitions **)
    40 (*mapping a relation over a list*)
    41 time_use     "ex/rmap.ML";
    42 (*completeness of propositional logic*)
    43 time_use     "ex/prop.ML";
    44 time_use_thy "ex/proplog";
    45 (*two Coq examples by Ch. Paulin-Mohring*)
    46 time_use     "ex/listn.ML";
    47 time_use     "ex/acc.ML";
    48 (*Diamond property for combinatory logic*)
    49 time_use     "ex/comb.ML";
    50 time_use_thy "ex/contract0";
    51 time_use     "ex/parcontract.ML";
    52 time_use_thy "ex/primrec0";
    53 
    54 (** CoDatatypes **)
    55 time_use_thy "ex/LList";
    56 time_use     "ex/llist_eq.ML";
    57 time_use_thy "ex/llistfn";
    58 time_use     "ex/counit.ML";
    59 
    60 maketest"END: Root file for ZF Set Theory examples";