src/Tools/float.ML
changeset 67560 0fa87bd86566
parent 30161 c26e515f1c29
     1.1 --- a/src/Tools/float.ML	Thu Feb 01 13:55:10 2018 +0100
     1.2 +++ b/src/Tools/float.ML	Thu Feb 01 15:12:57 2018 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  fun ord (r, s) = sign (sub r s);
     1.6  
     1.7 -fun eq (r, s) = ord (r, s) = EQUAL;
     1.8 +val eq = is_equal o ord;
     1.9  
    1.10  fun min r s = case ord (r, s) of LESS => r | _ => s;
    1.11  fun max r s = case ord (r, s) of LESS => s | _ => r;