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