src/HOL/Real/float_arith.ML
changeset 23569 6be49c181c66
parent 23297 06f108974fa1
child 24584 01e83ffa6c54
     1.1 --- a/src/HOL/Real/float_arith.ML	Wed Jul 04 16:49:36 2007 +0200
     1.2 +++ b/src/HOL/Real/float_arith.ML	Wed Jul 04 17:21:02 2007 +0200
     1.3 @@ -85,8 +85,8 @@
     1.4  exception Floating_point of string;
     1.5  
     1.6  val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
     1.7 -val exp5 = Integer.pow 5;
     1.8 -val exp10 = Integer.pow 10;
     1.9 +fun exp5 x = Integer.pow x 5;
    1.10 +fun exp10 x = Integer.pow x 10;
    1.11  
    1.12  fun find_most_significant q r =
    1.13    let