src/HOL/Library/Abstract_Rat.thy
changeset 47162 9d7d919b9fd8
parent 44780 a13cdb1e9e08
child 50282 fe4d4bb9f4c2
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:34:36 2012 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Tue Mar 27 15:40:11 2012 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4      from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
     1.5      have gpos: "?g > 0" by arith
     1.6      have gdvd: "?g dvd a" "?g dvd b" by arith+
     1.7 -    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
     1.8 +    from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz
     1.9      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    1.10      from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    1.11      from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
    1.12 @@ -56,7 +56,7 @@
    1.13        assume b: "b < 0"
    1.14        { assume b': "?b' \<ge> 0"
    1.15          from gpos have th: "?g \<ge> 0" by arith
    1.16 -        from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
    1.17 +        from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)]
    1.18          have False using b by arith }
    1.19        hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
    1.20        from anz bnz nz' b b' gp1 have ?thesis