1 (* Title: HOL/Real/float_arith.ML
1 (* Title: HOL/Tools/float_arith.ML
2 ID: $Id$
3 Author: Steven Obua
2 Author: Steven Obua
4 *)
3 *)
5
4
6 signature FLOAT_ARITH =
5 signature FLOAT_ARITH =
7 sig
6 sig