src/HOL/Nat.thy
changeset 53374 a14d2a854c02
parent 52729 412c9e0381a1
child 53986 a269577d97c0
     1.1 --- a/src/HOL/Nat.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -1888,8 +1888,8 @@
     1.4  proof -
     1.5    have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
     1.6      by (auto elim: dvd_plusE)
     1.7 -  also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
     1.8 -  also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
     1.9 +  also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
    1.10 +  also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
    1.11    also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
    1.12    finally show ?thesis .
    1.13  qed