zmod_zmult_zmult1 now subsumed by mod_mult_mult1
authorhaftmann
Fri Apr 17 08:34:52 2009 +0200 (2009-04-17)
changeset 30940663af91c0720
parent 30939 207ec81543f6
child 30941 705bb15b2365
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
src/HOL/Word/BinGeneral.thy
     1.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Apr 17 08:34:51 2009 +0200
     1.2 +++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 17 08:34:52 2009 +0200
     1.3 @@ -439,7 +439,7 @@
     1.4    apply clarsimp
     1.5    apply (simp add: bin_last_mod bin_rest_div Bit_def 
     1.6                cong: number_of_False_cong)
     1.7 -  apply (clarsimp simp: zmod_zmult_zmult1 [symmetric] 
     1.8 +  apply (clarsimp simp: mod_mult_mult1 [symmetric] 
     1.9           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    1.10    apply (rule trans [symmetric, OF _ emep1])
    1.11       apply auto