zmod_zmult_zmult1 now subsumed by mod_mult_mult1
authorhaftmann
Fri Apr 17 08:35:23 2009 +0200 (2009-04-17)
changeset 30943eb3dbbe971f6
parent 30942 1e246776f876
child 30944 7ac037c75c26
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
src/HOL/Word/BinOperations.thy
src/HOL/Word/Num_Lemmas.thy
     1.1 --- a/src/HOL/Word/BinOperations.thy	Fri Apr 17 08:34:54 2009 +0200
     1.2 +++ b/src/HOL/Word/BinOperations.thy	Fri Apr 17 08:35:23 2009 +0200
     1.3 @@ -641,7 +641,7 @@
     1.4    apply (simp add: bin_rest_div zdiv_zmult2_eq)
     1.5    apply (case_tac b rule: bin_exhaust)
     1.6    apply simp
     1.7 -  apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
     1.8 +  apply (simp add: Bit_def mod_mult_mult1 p1mod22k
     1.9                split: bit.split 
    1.10                cong: number_of_False_cong)
    1.11    done 
     2.1 --- a/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:34:54 2009 +0200
     2.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:35:23 2009 +0200
     2.3 @@ -66,7 +66,7 @@
     2.4    apply (safe dest!: even_equiv_def [THEN iffD1])
     2.5    apply (subst pos_zmod_mult_2)
     2.6     apply arith
     2.7 -  apply (simp add: zmod_zmult_zmult1)
     2.8 +  apply (simp add: mod_mult_mult1)
     2.9   done
    2.10  
    2.11  lemmas eme1p = emep1 [simplified add_commute]