1.1 --- a/src/ZF/ex/ROOT.ML	Fri Oct 22 13:43:45 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Fri Oct 22 13:44:27 1993 +0100
     1.3 @@ -41,18 +41,18 @@
     1.4  time_use     "ex/rmap.ML";
     1.5  (*completeness of propositional logic*)
     1.6  time_use     "ex/prop.ML";
     1.7 -time_use_thy "ex/propthms";
     1.8 +time_use_thy "ex/proplog";
     1.9  (*two Coq examples by Ch. Paulin-Mohring*)
    1.10  time_use     "ex/listn.ML";
    1.11  time_use     "ex/acc.ML";
    1.12  (*Diamond property for combinatory logic*)
    1.13  time_use     "ex/comb.ML";
    1.14 -time_use_thy "ex/contract";
    1.15 +time_use_thy "ex/contract0";
    1.16  time_use     "ex/parcontract.ML";
    1.17 -time_use_thy "ex/primrec";
    1.18 +time_use_thy "ex/primrec0";
    1.19  
    1.20  (** Co-Datatypes **)
    1.21 -time_use     "ex/llist.ML";
    1.22 +time_use_thy "ex/LList";
    1.23  time_use     "ex/llist_eq.ML";
    1.24  time_use_thy "ex/llistfn";
    1.25