diff -r 01906e4644e0 -r e30c23731c2d src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Wed Aug 17 10:34:44 1994 +0200 +++ b/src/ZF/ex/ROOT.ML Wed Aug 17 10:38:37 1994 +0200 @@ -16,7 +16,9 @@ time_use "ex/misc.ML"; time_use_thy "ex/Ramsey"; -(*Equivalence classes; integers; Binary integer arithmetic*) +(*Integers & Binary integer arithmetic*) +use "ex/twos_compl.ML"; (*can delete after autoloader change + and addition of "twos_compl" to Bin.thy*) time_use_thy "ex/Bin"; (** Datatypes **)