# HG changeset patch
# User haftmann
# Date 1239950123 -7200
# Node ID eb3dbbe971f618a457e074b98cea81cfed245670
# Parent  1e246776f876cb5bb20fa56cde52e3d92770a73f
zmod_zmult_zmult1 now subsumed by mod_mult_mult1

diff -r 1e246776f876 -r eb3dbbe971f6 src/HOL/Word/BinOperations.thy
--- 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 
diff -r 1e246776f876 -r eb3dbbe971f6 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:34:54 2009 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Fri Apr 17 08:35:23 2009 +0200
@@ -66,7 +66,7 @@
   apply (safe dest!: even_equiv_def [THEN iffD1])
   apply (subst pos_zmod_mult_2)
    apply arith
-  apply (simp add: zmod_zmult_zmult1)
+  apply (simp add: mod_mult_mult1)
  done
 
 lemmas eme1p = emep1 [simplified add_commute]