src/Tools/float.ML
changeset 23297 06f108974fa1
parent 23261 85f27f79232f
child 23520 483fe92f00c1
     1.1 --- a/src/Tools/float.ML	Fri Jun 08 18:13:58 2007 +0200
     1.2 +++ b/src/Tools/float.ML	Sat Jun 09 00:28:46 2007 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  type float = integer * integer;
     1.6  
     1.7 -val zero = (Integer.zero, Integer.zero);
     1.8 +val zero: float = (0, 0);
     1.9  
    1.10  fun add (a1, b1) (a2, b2) =
    1.11    if Integer.cmp (b1, b2) = LESS then
    1.12 @@ -54,7 +54,7 @@
    1.13  fun min r s = case cmp (r, s) of LESS => r | _ => s;
    1.14  fun max r s = case cmp (r, s) of LESS => s | _ => r;
    1.15  
    1.16 -fun positive_part (a, b) = (Integer.max Integer.zero a, b);
    1.17 -fun negative_part (a, b) = (Integer.min Integer.zero a, b);
    1.18 +fun positive_part (a, b) = (Integer.max 0 a, b);
    1.19 +fun negative_part (a, b) = (Integer.min 0 a, b);
    1.20  
    1.21  end;