--- a/src/HOL/Integ/IntArith.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/IntArith.thy Thu May 17 19:49:40 2007 +0200
@@ -7,7 +7,7 @@
theory IntArith
imports Numeral "../Wellfounded_Relations"
-uses ("int_arith1.ML")
+uses "~~/src/Provers/Arith/assoc_fold.ML" ("int_arith1.ML")
begin
text{*Duplicate: can't understand why it's necessary*}
@@ -103,7 +103,6 @@
max_def[of "number_of u" "1::int", standard, simp]
min_def[of "number_of u" "1::int", standard, simp]
-
use "int_arith1.ML"
setup int_arith_setup
@@ -394,7 +393,7 @@
done
-subsection {* Legavy ML bindings *}
+subsection {* Legacy ML bindings *}
ML {*
val of_int_number_of_eq = @{thm of_int_number_of_eq};