Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/Word.thy
changeset 47168 8395d7d63fc8
parent 47108 2a1953f0d20d
child 47372 9ab4e22dac7b 
--- a/src/HOL/Word/Word.thy	Tue Mar 27 20:19:23 2012 +0200
+++ b/src/HOL/Word/Word.thy	Tue Mar 27 21:48:26 2012 +0200
@@ -4465,9 +4465,9 @@
       and 4: "x' - y' = z'"
   shows "(x - y) mod b = z' mod b'"
   using assms
-  apply (subst zmod_zsub_left_eq)
-  apply (subst zmod_zsub_right_eq)
-  apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric])
+  apply (subst mod_diff_left_eq)
+  apply (subst mod_diff_right_eq)
+  apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
   done
 
 lemma word_induct_less:
isabelle