src/ZF/ROOT.ML
changeset 15481 fc075ae929e4
parent 12715 f7299128cd7d
child 16483 ace3c2b95353
     1.1 --- a/src/ZF/ROOT.ML	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -18,9 +18,6 @@
     1.4  (*syntax for old-style theory sections*)
     1.5  use "thy_syntax";
     1.6  
     1.7 -use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.8 -use "~~/src/Provers/Arith/combine_numerals.ML";
     1.9 -
    1.10  with_path "Integ" use_thy "Main_ZFC";
    1.11  
    1.12  print_depth 8;