author | haftmann |
Fri, 17 Apr 2009 08:34:52 +0200 | |
changeset 30940 | 663af91c0720 |
parent 30939 | 207ec81543f6 |
child 30941 | 705bb15b2365 |
--- a/src/HOL/Word/BinGeneral.thy Fri Apr 17 08:34:51 2009 +0200 +++ b/src/HOL/Word/BinGeneral.thy Fri Apr 17 08:34:52 2009 +0200 @@ -439,7 +439,7 @@ apply clarsimp apply (simp add: bin_last_mod bin_rest_div Bit_def cong: number_of_False_cong) - apply (clarsimp simp: zmod_zmult_zmult1 [symmetric] + apply (clarsimp simp: mod_mult_mult1 [symmetric] zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) apply (rule trans [symmetric, OF _ emep1]) apply auto