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
```