tuned;
authorwenzelm
Fri Nov 09 23:44:48 2001 +0100 (2001-11-09)
changeset 12133f314630235a4
parent 12132 1ef58b332ca9
child 12134 7049eead7a50
tuned;
src/ZF/ROOT.ML
     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