src/ZF/ex/ROOT.ML
changeset 34 747f1aad03cf
parent 16 0b033d50ca1c
child 56 2caa6f49f06e
     1.1 --- a/src/ZF/ex/ROOT.ML	Wed Oct 06 14:21:36 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Wed Oct 06 14:45:04 1993 +0100
     1.3 @@ -20,18 +20,18 @@
     1.4  (*Binary integer arithmetic*)
     1.5  use          "ex/twos-compl.ML";
     1.6  time_use     "ex/bin.ML";
     1.7 -time_use_thy "ex/bin-fn";
     1.8 +time_use_thy "ex/binfn";
     1.9  
    1.10  (** Datatypes **)
    1.11  (*binary trees*)
    1.12  time_use     "ex/bt.ML";
    1.13 -time_use_thy "ex/bt-fn";
    1.14 +time_use_thy "ex/bt_fn";
    1.15  (*terms: recursion over the list functor*)
    1.16  time_use     "ex/term.ML";
    1.17 -time_use_thy "ex/term-fn";
    1.18 +time_use_thy "ex/termfn";
    1.19  (*trees/forests: mutual recursion*)
    1.20  time_use     "ex/tf.ML";
    1.21 -time_use_thy "ex/tf-fn";
    1.22 +time_use_thy "ex/tf_fn";
    1.23  (*Enormous enumeration type -- could be even bigger?*)
    1.24  time_use     "ex/enum.ML";
    1.25  
    1.26 @@ -40,7 +40,7 @@
    1.27  time_use     "ex/rmap.ML";
    1.28  (*completeness of propositional logic*)
    1.29  time_use     "ex/prop.ML";
    1.30 -time_use_thy "ex/prop-log";
    1.31 +time_use_thy "ex/propthms";
    1.32  (*two Coq examples by Ch. Paulin-Mohring*)
    1.33  time_use     "ex/listn.ML";
    1.34  time_use     "ex/acc.ML";
    1.35 @@ -52,7 +52,8 @@
    1.36  
    1.37  (** Co-Datatypes **)
    1.38  time_use     "ex/llist.ML";
    1.39 -time_use_thy "ex/llist-fn";
    1.40 +time_use     "ex/llist_eq.ML";
    1.41 +time_use_thy "ex/llistfn";
    1.42  
    1.43  
    1.44  maketest"END: Root file for ZF Set Theory examples";