src/ZF/ROOT.ML
changeset 9548 15bee2731e43
parent 9211 6236c5285bd8
child 9570 e16e168984e1
     1.1 --- a/src/ZF/ROOT.ML	Mon Aug 07 10:29:04 2000 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Mon Aug 07 10:29:54 2000 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4  (*Add user sections for inductive/datatype definitions*)
     1.5  use     "thy_syntax";
     1.6  
     1.7 +use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.8 +
     1.9  use_thy "ZF";
    1.10  use     "Tools/typechk";
    1.11  use_thy "mono";