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:34:52 +0200
changeset 30940 663af91c0720
parent 30939 207ec81543f6
child 30941 705bb15b2365
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
src/HOL/Word/BinGeneral.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Word/BinGeneral.thy	Fri Apr 17 08:34:51 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 17 08:34:52 2009 +0200
@@ -439,7 +439,7 @@
   apply clarsimp
   apply (simp add: bin_last_mod bin_rest_div Bit_def 
               cong: number_of_False_cong)
-  apply (clarsimp simp: zmod_zmult_zmult1 [symmetric] 
+  apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   apply (rule trans [symmetric, OF _ emep1])
      apply auto
isabelle