diff -r 6b2c0681ef28 -r e138d96ed083 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Nov 23 13:00:00 2017 +0000
+++ b/src/HOL/Rings.thy	Thu Nov 23 17:03:20 2017 +0000
@@ -1699,17 +1699,15 @@
   using div_mult_mod_eq [of a a] by simp
 
 lemma dvd_imp_mod_0 [simp]:
-  assumes "a dvd b"
-  shows "b mod a = 0"
-  using assms minus_div_mult_eq_mod [of b a] by simp
+  "b mod a = 0" if "a dvd b"
+  using that minus_div_mult_eq_mod [of b a] by simp
 
 lemma mod_0_imp_dvd: 
-  assumes "a mod b = 0"
-  shows   "b dvd a"
+  "b dvd a" if "a mod b = 0"
 proof -
-  have "b dvd ((a div b) * b)" by simp
+  have "b dvd (a div b) * b" by simp
   also have "(a div b) * b = a"
-    using div_mult_mod_eq [of a b] by (simp add: assms)
+    using div_mult_mod_eq [of a b] by (simp add: that)
   finally show ?thesis .
 qed