--- 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 \<longleftrightarrow> m dvd r * m + (n - q)"
by (auto elim: dvd_plusE)
- also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
- also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
finally show ?thesis .
qed