changed use_thy's parameter to exact theory name
authorclasohm
Tue Nov 16 14:26:15 1993 +0100 (1993-11-16)
changeset 125bba27d15d76e
parent 124 858ab9a9b047
child 126 0b0055b3ccfe
changed use_thy's parameter to exact theory name
src/ZF/ex/ROOT.ML
     1.1 --- a/src/ZF/ex/ROOT.ML	Tue Nov 16 14:24:21 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Tue Nov 16 14:26:15 1993 +0100
     1.3 @@ -11,27 +11,29 @@
     1.4  writeln"Root file for ZF Set Theory examples";
     1.5  proof_timing := true;
     1.6  
     1.7 +loadpath := [".", "ex"];
     1.8 +
     1.9  time_use     "ex/misc.ML";
    1.10 -time_use_thy "ex/ramsey";
    1.11 +time_use_thy "ex/Ramsey";
    1.12  
    1.13  (*Equivalence classes and integers*)
    1.14 -time_use_thy "ex/equiv";
    1.15 -time_use_thy "ex/integ";
    1.16 +time_use_thy "ex/Equiv";
    1.17 +time_use_thy "ex/Integ";
    1.18  (*Binary integer arithmetic*)
    1.19  use          "ex/twos_compl.ML";
    1.20  time_use     "ex/bin.ML";
    1.21 -time_use_thy "ex/binfn";
    1.22 +time_use_thy "ex/BinFn";
    1.23  
    1.24  (** Datatypes **)
    1.25  (*binary trees*)
    1.26  time_use     "ex/bt.ML";
    1.27 -time_use_thy "ex/bt_fn";
    1.28 +time_use_thy "ex/BT_Fn";
    1.29  (*terms: recursion over the list functor*)
    1.30  time_use     "ex/term.ML";
    1.31 -time_use_thy "ex/termfn";
    1.32 +time_use_thy "ex/TermFn";
    1.33  (*trees/forests: mutual recursion*)
    1.34  time_use     "ex/tf.ML";
    1.35 -time_use_thy "ex/tf_fn";
    1.36 +time_use_thy "ex/TF_Fn";
    1.37  (*Sample datatype; enormous enumeration type*)
    1.38  time_use     "ex/data.ML";
    1.39  time_use     "ex/enum.ML";
    1.40 @@ -41,20 +43,20 @@
    1.41  time_use     "ex/rmap.ML";
    1.42  (*completeness of propositional logic*)
    1.43  time_use     "ex/prop.ML";
    1.44 -time_use_thy "ex/proplog";
    1.45 +time_use_thy "ex/PropLog";
    1.46  (*two Coq examples by Ch. Paulin-Mohring*)
    1.47  time_use     "ex/listn.ML";
    1.48  time_use     "ex/acc.ML";
    1.49  (*Diamond property for combinatory logic*)
    1.50  time_use     "ex/comb.ML";
    1.51 -time_use_thy "ex/contract0";
    1.52 +time_use_thy "ex/Contract0";
    1.53  time_use     "ex/parcontract.ML";
    1.54 -time_use_thy "ex/primrec0";
    1.55 +time_use_thy "ex/Primrec0";
    1.56  
    1.57  (** CoDatatypes **)
    1.58  time_use_thy "ex/LList";
    1.59  time_use     "ex/llist_eq.ML";
    1.60 -time_use_thy "ex/llistfn";
    1.61 +time_use_thy "ex/LListFn";
    1.62  time_use     "ex/counit.ML";
    1.63  
    1.64  maketest"END: Root file for ZF Set Theory examples";