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

src/HOL/Rat.thy

changeset 58834 | 773b378d9313 |

parent 58410 | 6d46ad54a2ab |

child 58889 | 5b7a9633cfa8 |

1.1 --- a/src/HOL/Rat.thy Thu Oct 30 16:36:44 2014 +0000 1.2 +++ b/src/HOL/Rat.thy Thu Oct 30 21:02:01 2014 +0100 1.3 @@ -73,8 +73,8 @@ 1.4 let ?a = "a div gcd a b" 1.5 let ?b = "b div gcd a b" 1.6 from `b \<noteq> 0` have "?b * gcd a b = b" 1.7 - by (simp add: dvd_div_mult_self) 1.8 - with `b \<noteq> 0` have "?b \<noteq> 0" by auto 1.9 + by simp 1.10 + with `b \<noteq> 0` have "?b \<noteq> 0" by fastforce 1.11 from `q = Fract a b` `b \<noteq> 0` `?b \<noteq> 0` have q: "q = Fract ?a ?b" 1.12 by (simp add: eq_rat dvd_div_mult mult.commute [of a]) 1.13 from `b \<noteq> 0` have coprime: "coprime ?a ?b" 1.14 @@ -253,7 +253,8 @@ 1.15 case False 1.16 moreover have "b div gcd a b * gcd a b = b" 1.17 by (rule dvd_div_mult_self) simp 1.18 - ultimately have "b div gcd a b \<noteq> 0" by auto 1.19 + ultimately have "b div gcd a b * gcd a b \<noteq> 0" by simp 1.20 + then have "b div gcd a b \<noteq> 0" by fastforce 1.21 with False show ?thesis by (simp add: eq_rat dvd_div_mult mult.commute [of a]) 1.22 qed 1.23