src/ZF/ArithSimp.thy

--- a/src/ZF/ArithSimp.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/ZF/ArithSimp.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,11 +7,13 @@
 
 theory ArithSimp
 imports Arith
-uses "~~/src/Provers/Arith/cancel_numerals.ML"
-      "~~/src/Provers/Arith/combine_numerals.ML"
-      "arith_data.ML"
 begin
 
+ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
+ML_file "~~/src/Provers/Arith/combine_numerals.ML"
+ML_file "arith_data.ML"
+
+
 subsection{*Difference*}
 
 lemma diff_self_eq_0 [simp]: "m #- m = 0"