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