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