src/HOL/Real/float_arith.ML
changeset 25300 bc3a1c964704
parent 24630 351a308ab58d
     1.1 --- a/src/HOL/Real/float_arith.ML	Mon Nov 05 22:51:16 2007 +0100
     1.2 +++ b/src/HOL/Real/float_arith.ML	Mon Nov 05 22:53:38 2007 +0100
     1.3 @@ -87,6 +87,7 @@
     1.4  val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
     1.5  fun exp5 x = Integer.pow x 5;
     1.6  fun exp10 x = Integer.pow x 10;
     1.7 +fun exp2 x = Integer.pow x 2;
     1.8  
     1.9  fun find_most_significant q r =
    1.10    let
    1.11 @@ -101,7 +102,7 @@
    1.12          (q * exp10 (r - r') - q', r')
    1.13      fun bin2dec d =
    1.14        if 0 <= d then
    1.15 -        (Integer.square d, 0)
    1.16 +        (exp2 d, 0)
    1.17        else
    1.18          (exp5 (~ d), d)
    1.19  
    1.20 @@ -133,7 +134,7 @@
    1.21  fun approx_dec_by_bin n (q,r) =
    1.22    let
    1.23      fun addseq acc d' [] = acc
    1.24 -      | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds
    1.25 +      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
    1.26  
    1.27      fun seq2bin [] = (0, 0)
    1.28        | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
    1.29 @@ -151,7 +152,7 @@
    1.30              let
    1.31                val d' = d0 - precision
    1.32                val x1 = seq2bin (d_seq)
    1.33 -              val x2 = (fst x1 * Integer.square (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
    1.34 +              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
    1.35              in
    1.36                (x1, x2)
    1.37              end