changeset 24584 | 01e83ffa6c54 |
parent 23520 | 483fe92f00c1 |
child 24630 | 351a308ab58d |
24583:d77e4d48e497 | 24584:01e83ffa6c54 |
---|---|
1 (* Title: Pure/General/float.ML |
1 (* Title: Tools/float.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua, Florian Haftmann, TU Muenchen |
3 Author: Steven Obua, Florian Haftmann, TU Muenchen |
4 |
4 |
5 Implementation of real numbers as mantisse-exponent pairs. |
5 Implementation of real numbers as mantisse-exponent pairs. |
6 *) |
6 *) |