src/HOL/Code_Numeral.thy
changeset 44821 a92f65e174cf
parent 39818 ff9e9d5ac171
child 45694 4a8743618257
     1.1 --- a/src/HOL/Code_Numeral.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -274,7 +274,7 @@
     1.4    then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
     1.5      by simp
     1.6    then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
     1.7 -    unfolding int_mult zadd_int [symmetric] by simp
     1.8 +    unfolding of_nat_mult of_nat_add by simp
     1.9    then show ?thesis by (auto simp add: int_of_def mult_ac)
    1.10  qed
    1.11