src/ZF/ROOT.ML
changeset 9570 e16e168984e1
parent 9548 15bee2731e43
child 12133 f314630235a4
     1.1 --- a/src/ZF/ROOT.ML	Thu Aug 10 00:45:23 2000 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Thu Aug 10 11:27:34 2000 +0200
     1.3 @@ -19,9 +19,8 @@
     1.4  use     "thy_syntax";
     1.5  
     1.6  use "~~/src/Provers/Arith/cancel_numerals.ML";
     1.7 +use "~~/src/Provers/Arith/combine_numerals.ML";
     1.8  
     1.9 -use_thy "ZF";
    1.10 -use     "Tools/typechk";
    1.11  use_thy "mono";
    1.12  use     "ind_syntax";
    1.13  use     "Tools/cartprod";
    1.14 @@ -32,6 +31,7 @@
    1.15  use_thy "QUniv";
    1.16  use     "Tools/datatype_package";
    1.17  
    1.18 +use     "Tools/numeral_syntax";
    1.19  (*the all-in-one theory*)
    1.20  with_path "Integ" use_thy "Main";
    1.21