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

src/HOL/ex/Sqrt.thy

changeset 61649 | 268d88ec9087 |

parent 60690 | a9e45c9588c3 |

child 61762 | d50b993b4fb9 |

1.1 --- a/src/HOL/ex/Sqrt.thy Thu Nov 12 11:22:26 2015 +0100 1.2 +++ b/src/HOL/ex/Sqrt.thy Fri Nov 13 12:27:13 2015 +0000 1.3 @@ -26,7 +26,7 @@ 1.4 by (auto simp add: power2_eq_square) 1.5 also have "(sqrt p)\<^sup>2 = p" by simp 1.6 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp 1.7 - finally show ?thesis .. 1.8 + finally show ?thesis using of_nat_eq_iff by blast 1.9 qed 1.10 have "p dvd m \<and> p dvd n" 1.11 proof 1.12 @@ -69,7 +69,7 @@ 1.13 by (auto simp add: power2_eq_square) 1.14 also have "(sqrt p)\<^sup>2 = p" by simp 1.15 also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp 1.16 - finally have eq: "m\<^sup>2 = p * n\<^sup>2" .. 1.17 + finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast 1.18 then have "p dvd m\<^sup>2" .. 1.19 with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat) 1.20 then obtain k where "m = p * k" ..