author | obua |
Wed, 04 Jul 2007 17:21:02 +0200 | |
changeset 23569 | 6be49c181c66 |
parent 23568 | afecdba16452 |
child 23570 | 37532c9df22c |
--- a/src/HOL/Real/float_arith.ML Wed Jul 04 16:49:36 2007 +0200 +++ b/src/HOL/Real/float_arith.ML Wed Jul 04 17:21:02 2007 +0200 @@ -85,8 +85,8 @@ exception Floating_point of string; val ln2_10 = Math.ln 10.0 / Math.ln 2.0; -val exp5 = Integer.pow 5; -val exp10 = Integer.pow 10; +fun exp5 x = Integer.pow x 5; +fun exp10 x = Integer.pow x 10; fun find_most_significant q r = let