changeset 30943 | eb3dbbe971f6 |
parent 29631 | 3aa049e5f156 |
child 37654 | 8e33b9d04a82 |
--- a/src/HOL/Word/BinOperations.thy Fri Apr 17 08:34:54 2009 +0200 +++ b/src/HOL/Word/BinOperations.thy Fri Apr 17 08:35:23 2009 +0200 @@ -641,7 +641,7 @@ apply (simp add: bin_rest_div zdiv_zmult2_eq) apply (case_tac b rule: bin_exhaust) apply simp - apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k + apply (simp add: Bit_def mod_mult_mult1 p1mod22k split: bit.split cong: number_of_False_cong) done