src/HOL/Library/Float.thy
changeset 46670 e9aa6d151329
parent 46573 8c4c5c8dcf7a
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Library/Float.thy	Sat Feb 25 09:07:37 2012 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Sat Feb 25 09:07:39 2012 +0100
     1.3 @@ -670,7 +670,7 @@
     1.4    let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
     1.5    show ?thesis 
     1.6    proof (cases "?X mod y = 0")
     1.7 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
     1.8 +    case True hence "y dvd ?X" using `0 < y` by auto
     1.9      from real_of_int_div[OF this]
    1.10      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    1.11      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
    1.12 @@ -702,7 +702,7 @@
    1.13    let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
    1.14    show ?thesis
    1.15    proof (cases "?X mod y = 0")
    1.16 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
    1.17 +    case True hence "y dvd ?X" using `0 < y` by auto
    1.18      from real_of_int_div[OF this]
    1.19      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    1.20      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
    1.21 @@ -757,7 +757,7 @@
    1.22    let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
    1.23    show ?thesis
    1.24    proof (cases "?X mod y = 0")
    1.25 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
    1.26 +    case True hence "y dvd ?X" using `0 < y` by auto
    1.27      from real_of_int_div[OF this]
    1.28      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    1.29      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto