ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
authorlcp
Wed Dec 01 17:40:27 1993 +0100 (1993-12-01)
changeset 1808962c2b0dc2b
parent 179 ceb948cefb93
child 181 9c2db771f224
ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted
them, to make the most of the load-path mechanism. (use_thy adds the new
theory to the list of loaded theories.)
src/ZF/ex/ROOT.ML
     1.1 --- a/src/ZF/ex/ROOT.ML	Wed Dec 01 13:00:04 1993 +0100
     1.2 +++ b/src/ZF/ex/ROOT.ML	Wed Dec 01 17:40:27 1993 +0100
     1.3 @@ -21,41 +21,27 @@
     1.4  time_use_thy "ex/Integ";
     1.5  (*Binary integer arithmetic*)
     1.6  use          "ex/twos_compl.ML";
     1.7 -time_use     "ex/bin.ML";
     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 -(*terms: recursion over the list functor*)
    1.15 -time_use     "ex/term.ML";
    1.16 -time_use_thy "ex/TermFn";
    1.17 -(*trees/forests: mutual recursion*)
    1.18 -time_use     "ex/tf.ML";
    1.19 -time_use_thy "ex/TF_Fn";
    1.20 -(*Sample datatype; enormous enumeration type*)
    1.21 -time_use     "ex/data.ML";
    1.22 -time_use     "ex/enum.ML";
    1.23 +time_use_thy "ex/BT_Fn";	(*binary trees*)
    1.24 +time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
    1.25 +time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
    1.26 +time_use_thy "ex/Data";		(*Sample datatype*)
    1.27 +time_use_thy "ex/Enum";		(*Enormous enumeration type*)
    1.28  
    1.29  (** Inductive definitions **)
    1.30 -(*mapping a relation over a list*)
    1.31 -time_use     "ex/rmap.ML";
    1.32 -(*completeness of propositional logic*)
    1.33 -time_use     "ex/prop.ML";
    1.34 -time_use_thy "ex/PropLog";
    1.35 +time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
    1.36 +time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
    1.37  (*two Coq examples by Ch. Paulin-Mohring*)
    1.38 -time_use     "ex/listn.ML";
    1.39 -time_use     "ex/acc.ML";
    1.40 -(*Diamond property for combinatory logic*)
    1.41 -time_use     "ex/comb.ML";
    1.42 -time_use_thy "ex/Contract0";
    1.43 -time_use     "ex/parcontract.ML";
    1.44 +time_use_thy "ex/ListN";
    1.45 +time_use_thy "ex/Acc";
    1.46 +time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
    1.47 +time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
    1.48  time_use_thy "ex/Primrec0";
    1.49  
    1.50  (** CoDatatypes **)
    1.51  time_use_thy "ex/LList";
    1.52 -time_use     "ex/llist_eq.ML";
    1.53  time_use_thy "ex/LListFn";
    1.54  time_use     "ex/counit.ML";
    1.55