src/HOL/Integ/IntArith.thy

 
 header {* Integer arithmetic *}
 
 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*}
 declare numeral_0_eq_0 [simp]
 

  min_def[of "number_of u" "0::int", standard, simp]
  max_def[of "1::int" "number_of v", standard, simp]
  min_def[of "1::int" "number_of v", standard, simp]
  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
 
 

  apply (simp add: mult_commute [of m]) 
  apply (frule pos_zmult_eq_1_iff_lemma, auto) 
 done
 
 
-subsection {* Legavy ML bindings *}
+subsection {* Legacy ML bindings *}
 
 ML {*
 val of_int_number_of_eq = @{thm of_int_number_of_eq};
 val nat_0 = @{thm nat_0};
 val nat_1 = @{thm nat_1};