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/Number_Theory/Euclidean_Algorithm.thy
changeset 64240 eabf80376aab
parent 64177 006f303fb173
child 64242 93c6f0da5c70 
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:03 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Oct 16 09:31:04 2016 +0200
@@ -26,7 +26,7 @@
     "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (a * b)"
 begin
 
-lemma zero_mod_left [simp]: "0 mod a = 0"
+lemma mod_0 [simp]: "0 mod a = 0"
   using mod_div_equality [of 0 a] by simp
 
 lemma dvd_mod_iff:
isabelle