Adapted FloatArith.ML to SMLNJ 10.0.7
authorobua
Wed, 08 Sep 2004 13:55:51 +0200
changeset 15189 9cfbc392918c
parent 15188 9d57263faf9e
child 15190 b6788dbd2ef9
Adapted FloatArith.ML to SMLNJ 10.0.7
src/HOL/Matrix/FloatArith.ML
--- a/src/HOL/Matrix/FloatArith.ML	Tue Sep 07 16:02:42 2004 +0200
+++ b/src/HOL/Matrix/FloatArith.ML	Wed Sep 08 13:55:51 2004 +0200
@@ -28,13 +28,13 @@
 fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
 
 fun add (a1, b1) (a2, b2) = 
-    if b1 < b2 then
+    if IntInf.< (b1, b2) then
 	(iadd a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
 	(iadd (imul a1 (ipow2 (isub b1 b2))) a2, b2)
 
 fun sub (a1, b1) (a2, b2) = 
-    if b1 < b2 then
+    if IntInf.< (b1, b2) then
 	(isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
     else
 	(isub (imul a1 (ipow2 (isub b1 b2))) a2, b2)