src/HOL/Code_Numeral.thy
changeset 57512 cc97b347b301
parent 56846 9df717fef2bb
child 58306 117ba6cbe414
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -494,7 +494,7 @@
     1.4      show "k = integer_of_int (int_of_integer k)" by simp
     1.5    qed
     1.6    moreover have "2 * (j div 2) = j - j mod 2"
     1.7 -    by (simp add: zmult_div_cancel mult_commute)
     1.8 +    by (simp add: zmult_div_cancel mult.commute)
     1.9    ultimately show ?thesis
    1.10      by (auto simp add: split_def Let_def mod_integer_def nat_of_integer_def not_le
    1.11        nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)