--- a/src/HOL/Matrix/FloatArith.ML Mon Mar 07 16:55:36 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-structure FloatArith =
-struct
-
-type float = IntInf.int * IntInf.int
-
-val izero = IntInf.fromInt 0
-fun imul a b = IntInf.* (a,b)
-fun isub a b = IntInf.- (a,b)
-fun iadd a b = IntInf.+ (a,b)
-
-val floatzero = (izero, izero)
-
-fun positive_part (a,b) =
- (if IntInf.< (a,izero) then izero else a, b)
-
-fun negative_part (a,b) =
- (if IntInf.< (a,izero) then a else izero, b)
-
-fun is_negative (a,b) =
- if IntInf.< (a, izero) then true else false
-
-fun is_positive (a,b) =
- if IntInf.< (izero, a) then true else false
-
-fun is_zero (a,b) =
- if a = izero then true else false
-
-fun ipow2 a = IntInf.pow ((IntInf.fromInt 2), IntInf.toInt a)
-
-fun add (a1, b1) (a2, b2) =
- 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 IntInf.< (b1, b2) then
- (isub a1 (imul a2 (ipow2 (isub b2 b1))), b1)
- else
- (isub (imul a1 (ipow2 (isub b1 b2))) a2, b2)
-
-fun neg (a, b) = (IntInf.~ a, b)
-
-fun is_equal a b = is_zero (sub a b)
-
-fun is_less a b = is_negative (sub a b)
-
-fun max a b = if is_less a b then b else a
-
-fun min a b = if is_less a b then a else b
-
-fun abs a = if is_negative a then neg a else a
-
-fun mul (a1, b1) (a2, b2) = (imul a1 a2, iadd b1 b2)
-
-end;