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