# HG changeset patch
# User haftmann
# Date 1511456600 0
# Node ID e138d96ed08325e1322319dd9ebb2e6f2680ff8c
# Parent  6b2c0681ef2853041243b25239cec8c841b6a02e
tuned

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