src/Tools/float.ML
changeset 70586 57df8a85317a
parent 67560 0fa87bd86566
equal deleted inserted replaced
70583:17909568216e 70586:57df8a85317a
     7 signature FLOAT =
     7 signature FLOAT =
     8 sig
     8 sig
     9   type float = int * int
     9   type float = int * int
    10   val zero: float
    10   val zero: float
    11   val eq: float * float -> bool
    11   val eq: float * float -> bool
    12   val ord: float * float -> order
    12   val ord: float ord
    13   val sign: float -> order
    13   val sign: float -> order
    14   val min: float -> float -> float
    14   val min: float -> float -> float
    15   val max: float -> float -> float
    15   val max: float -> float -> float
    16   val add: float -> float -> float
    16   val add: float -> float -> float
    17   val sub: float -> float -> float
    17   val sub: float -> float -> float