# HG changeset patch
# User lcp
# Date 754764027 -3600
# Node ID 8962c2b0dc2b6b7e3f1027a8fe1b44e24a781f91
# Parent  ceb948cefb93dccb5cecf4157e2d6cc1c1c1fde5
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.)

diff -r ceb948cefb93 -r 8962c2b0dc2b src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Wed Dec 01 13:00:04 1993 +0100
+++ b/src/ZF/ex/ROOT.ML	Wed Dec 01 17:40:27 1993 +0100
@@ -21,41 +21,27 @@
 time_use_thy "ex/Integ";
 (*Binary integer arithmetic*)
 use          "ex/twos_compl.ML";
-time_use     "ex/bin.ML";
 time_use_thy "ex/BinFn";
 
 (** Datatypes **)
-(*binary trees*)
-time_use     "ex/bt.ML";
-time_use_thy "ex/BT_Fn";
-(*terms: recursion over the list functor*)
-time_use     "ex/term.ML";
-time_use_thy "ex/TermFn";
-(*trees/forests: mutual recursion*)
-time_use     "ex/tf.ML";
-time_use_thy "ex/TF_Fn";
-(*Sample datatype; enormous enumeration type*)
-time_use     "ex/data.ML";
-time_use     "ex/enum.ML";
+time_use_thy "ex/BT_Fn";	(*binary trees*)
+time_use_thy "ex/TermFn";	(*terms: recursion over the list functor*)
+time_use_thy "ex/TF_Fn";	(*trees/forests: mutual recursion*)
+time_use_thy "ex/Data";		(*Sample datatype*)
+time_use_thy "ex/Enum";		(*Enormous enumeration type*)
 
 (** Inductive definitions **)
-(*mapping a relation over a list*)
-time_use     "ex/rmap.ML";
-(*completeness of propositional logic*)
-time_use     "ex/prop.ML";
-time_use_thy "ex/PropLog";
+time_use_thy "ex/Rmap";		(*mapping a relation over a list*)
+time_use_thy "ex/PropLog";	(*completeness of propositional logic*)
 (*two Coq examples by Ch. Paulin-Mohring*)
-time_use     "ex/listn.ML";
-time_use     "ex/acc.ML";
-(*Diamond property for combinatory logic*)
-time_use     "ex/comb.ML";
-time_use_thy "ex/Contract0";
-time_use     "ex/parcontract.ML";
+time_use_thy "ex/ListN";
+time_use_thy "ex/Acc";
+time_use_thy "ex/Contract0";	(*Contraction relation for combinatory logic*)
+time_use_thy "ex/ParContract";	(*Diamond property for combinatory logic*)
 time_use_thy "ex/Primrec0";
 
 (** CoDatatypes **)
 time_use_thy "ex/LList";
-time_use     "ex/llist_eq.ML";
 time_use_thy "ex/LListFn";
 time_use     "ex/counit.ML";