# HG changeset patch
# User wenzelm
# Date 1005345888 -3600
# Node ID f314630235a45f1958e6fbe65d7a50f85b3e4ceb
# Parent  1ef58b332ca9afe1db29b5113cd8068df10d7493
tuned;

diff -r 1ef58b332ca9 -r f314630235a4 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Fri Nov 09 22:53:41 2001 +0100
+++ b/src/ZF/ROOT.ML	Fri Nov 09 23:44:48 2001 +0100
@@ -22,16 +22,16 @@
 use "~~/src/Provers/Arith/combine_numerals.ML";
 
 use_thy "mono";
-use     "ind_syntax";
-use     "Tools/cartprod";
+use     "ind_syntax.ML";
+use     "Tools/cartprod.ML";
 use_thy "Fixedpt";
-use     "Tools/inductive_package";
-use     "Tools/induct_tacs";
-use     "Tools/primrec_package";
+use     "Tools/inductive_package.ML";
+use     "Tools/induct_tacs.ML";
+use     "Tools/primrec_package.ML";
 use_thy "QUniv";
-use     "Tools/datatype_package";
+use     "Tools/datatype_package.ML";
 
-use     "Tools/numeral_syntax";
+use     "Tools/numeral_syntax.ML";
 (*the all-in-one theory*)
 with_path "Integ" use_thy "Main";