# 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";