diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Nat.thy Tue Sep 03 01:12:40 2013 +0200
@@ -1888,8 +1888,8 @@
proof -
have "m dvd n - q \ m dvd r * m + (n - q)"
by (auto elim: dvd_plusE)
- also with assms have "\ \ m dvd r * m + n - q" by simp
- also with assms have "\ \ m dvd (r * m - q) + n" by simp
+ also from assms have "\ \ m dvd r * m + n - q" by simp
+ also from assms have "\ \ m dvd (r * m - q) + n" by simp
also have "\ \ m dvd n + (r * m - q)" by (simp add: add_commute)
finally show ?thesis .
qed