src/ZF/ex/ROOT.ML
changeset 16 0b033d50ca1c
parent 0 a5a9c433f639
child 34 747f1aad03cf
     1.1 --- a/src/ZF/ex/ROOT.ML	Thu Sep 30 10:26:38 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Thu Sep 30 10:54:01 1993 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Executes all examples for Zermelo-Fraenkel Set Theory
     1.5  *)
     1.6  
     1.7 -ZF_build_completed;	(*Cause examples to fail if ZF did*)
     1.8 +ZF_build_completed;	(*Make examples fail if ZF did*)
     1.9  
    1.10  writeln"Root file for ZF Set Theory examples";
    1.11  proof_timing := true;
    1.12 @@ -36,6 +36,8 @@
    1.13  time_use     "ex/enum.ML";
    1.14  
    1.15  (** Inductive definitions **)
    1.16 +(*mapping a relation over a list*)
    1.17 +time_use     "ex/rmap.ML";
    1.18  (*completeness of propositional logic*)
    1.19  time_use     "ex/prop.ML";
    1.20  time_use_thy "ex/prop-log";
    1.21 @@ -46,6 +48,7 @@
    1.22  time_use     "ex/comb.ML";
    1.23  time_use_thy "ex/contract";
    1.24  time_use     "ex/parcontract.ML";
    1.25 +time_use_thy "ex/primrec";
    1.26  
    1.27  (** Co-Datatypes **)
    1.28  time_use     "ex/llist.ML";