summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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