diff -r 59d07a95be0e -r 733017b19de9 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:26 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:27 2017 +0000
@@ -139,7 +139,7 @@
 class euclidean_ring = idom_modulo + euclidean_semiring
 begin
 
-lemma dvd_diff_commute:
+lemma dvd_diff_commute [ac_simps]:
   "a dvd c - b \<longleftrightarrow> a dvd b - c"
 proof -
   have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"