src/HOL/Library/Code_Target_Int.thy
changeset 54227 63b441f49645
parent 53069 d165213e3924
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  proof -
     1.5    from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
     1.6    show ?thesis
     1.7 -    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
     1.8 +    by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1
     1.9        of_int_add [symmetric]) (simp add: * mult_commute)
    1.10  qed
    1.11