src/ZF/ex/ROOT.ML
author lcp
Fri May 06 15:35:35 1994 +0200 (1994-05-06)
changeset 365 796c5e305b31
parent 180 8962c2b0dc2b
child 489 0449a7f1add3
permissions -rw-r--r--
renaming/removal of filenames to correct case
     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/Data";		(*Sample datatype*)
    31 time_use_thy "ex/Enum";		(*Enormous enumeration type*)
    32 
    33 (** Inductive definitions **)
    34 time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
    35 time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
    36 (*two Coq examples by Ch. Paulin-Mohring*)
    37 time_use_thy "ex/ListN";
    38 time_use_thy "ex/Acc";
    39 time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
    40 time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
    41 time_use_thy "ex/Primrec0";
    42 
    43 (** CoDatatypes **)
    44 time_use_thy "ex/LList";
    45 time_use_thy "ex/LListFn";
    46 time_use     "ex/CoUnit.ML";
    47 
    48 maketest"END: Root file for ZF Set Theory examples";