# HG changeset patch
# User lcp
# Date 776968070 -7200
# Node ID 85d7ff169b9cb191dd00e9527fca18ea51aeb144
# Parent  e62519a8497d0a5ad36d677416f7ba3e8040b03e
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
removed some explicit loads by exploiting theory dependencies

diff -r e62519a8497d -r 85d7ff169b9c src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Mon Aug 15 18:25:27 1994 +0200
+++ b/src/ZF/ex/ROOT.ML	Mon Aug 15 18:27:50 1994 +0200
@@ -16,20 +16,16 @@
 time_use     "ex/misc.ML";
 time_use_thy "ex/Ramsey";
 
-(*Equivalence classes and integers*)
-time_use_thy "ex/Equiv";
-time_use_thy "ex/Integ";
-(*Binary integer arithmetic*)
-use          "ex/twos_compl.ML";
+(*Equivalence classes; integers; Binary integer arithmetic*)
 time_use_thy "ex/Bin";
 
 (** Datatypes **)
 time_use_thy "ex/BT";		(*binary trees*)
+time_use_thy "ex/Data";		(*Sample datatype*)
 time_use_thy "ex/Term";		(*terms: recursion over the list functor*)
 time_use_thy "ex/TF";		(*trees/forests: mutual recursion*)
 time_use_thy "ex/Ntree";	(*variable-branching trees; function demo*)
-time_use_thy "ex/Brouwer";	(*Brouwer ordinals: infinite-branching trees*)
-time_use_thy "ex/Data";		(*Sample datatype*)
+time_use_thy "ex/Brouwer";	(*Infinite-branching trees*)
 time_use_thy "ex/Enum";		(*Enormous enumeration type*)
 
 (** Inductive definitions **)
@@ -39,10 +35,10 @@
 time_use_thy "ex/ListN";
 time_use_thy "ex/Acc";
 time_use_thy "ex/Comb";		(*Combinatory Logic example*)
-time_use_thy "ex/Primrec";
+time_use_thy "ex/Primrec";	(*Primitive recursive functions*)
 
 (** CoDatatypes **)
 time_use_thy "ex/LList";
-time_use     "ex/CoUnit.ML";
+time_use_thy "ex/CoUnit";
 
 maketest"END: Root file for ZF Set Theory examples";