src/ZF/ROOT.ML
changeset 12133 f314630235a4
parent 9570 e16e168984e1
child 12175 5cf58a1799a7
     1.1 --- a/src/ZF/ROOT.ML	Fri Nov 09 22:53:41 2001 +0100
     1.2 +++ b/src/ZF/ROOT.ML	Fri Nov 09 23:44:48 2001 +0100
     1.3 @@ -22,16 +22,16 @@
     1.4  use "~~/src/Provers/Arith/combine_numerals.ML";
     1.5  
     1.6  use_thy "mono";
     1.7 -use     "ind_syntax";
     1.8 -use     "Tools/cartprod";
     1.9 +use     "ind_syntax.ML";
    1.10 +use     "Tools/cartprod.ML";
    1.11  use_thy "Fixedpt";
    1.12 -use     "Tools/inductive_package";
    1.13 -use     "Tools/induct_tacs";
    1.14 -use     "Tools/primrec_package";
    1.15 +use     "Tools/inductive_package.ML";
    1.16 +use     "Tools/induct_tacs.ML";
    1.17 +use     "Tools/primrec_package.ML";
    1.18  use_thy "QUniv";
    1.19 -use     "Tools/datatype_package";
    1.20 +use     "Tools/datatype_package.ML";
    1.21  
    1.22 -use     "Tools/numeral_syntax";
    1.23 +use     "Tools/numeral_syntax.ML";
    1.24  (*the all-in-one theory*)
    1.25  with_path "Integ" use_thy "Main";
    1.26