src/ZF/ex/ROOT.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 526 85d7ff169b9c
child 540 e30c23731c2d
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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; integers; Binary integer arithmetic*)
    20 time_use_thy "ex/Bin";
    21 
    22 (** Datatypes **)
    23 time_use_thy "ex/BT";		(*binary trees*)
    24 time_use_thy "ex/Data";		(*Sample datatype*)
    25 time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
    26 time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
    27 time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
    28 time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
    29 time_use_thy "ex/Enum";		(*Enormous enumeration type*)
    30 
    31 (** Inductive definitions **)
    32 time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
    33 time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
    34 (*two Coq examples by Christine Paulin-Mohring*)
    35 time_use_thy "ex/ListN";
    36 time_use_thy "ex/Acc";
    37 time_use_thy "ex/Comb";		(*Combinatory Logic example*)
    38 time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
    39 
    40 (** CoDatatypes **)
    41 time_use_thy "ex/LList";
    42 time_use_thy "ex/CoUnit";
    43 
    44 maketest"END: Root file for ZF Set Theory examples";