src/HOL/Library/Code_Target_Int.thy
changeset 57512 cc97b347b301
parent 55932 68c5104d2204
child 58099 7f232ae7de7c
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4    from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
     1.5    show ?thesis
     1.6      by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
     1.7 -      (simp add: * mult_commute)
     1.8 +      (simp add: * mult.commute)
     1.9  qed
    1.10  
    1.11  declare of_int_code_if [code]