src/HOL/Library/Float.thy
changeset 57512 cc97b347b301
parent 57492 74bf65a1910a
child 57862 8f074e6e22fc
     1.1 --- a/src/HOL/Library/Float.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -844,7 +844,7 @@
     1.4      hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
     1.5        by (auto simp: powr_minus)
     1.6      hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
     1.7 -    hence "?S \<le> real m" unfolding mult_assoc by auto
     1.8 +    hence "?S \<le> real m" unfolding mult.assoc by auto
     1.9      hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
    1.10      from this bitlen_bounds[OF `0 < m`, THEN conjunct2]
    1.11      have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans)