Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
authorhaftmann
Fri, 17 Apr 2009 08:35:23 +0200
changeset 30943 eb3dbbe971f6
parent 30942 1e246776f876
child 30944 7ac037c75c26
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
src/HOL/Word/BinOperations.thy file | annotate | diff | comparison | revisions
src/HOL/Word/Num_Lemmas.thy file | annotate | diff | comparison | revisions 
--- 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 
--- 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]
isabelle