equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow, TU Muenchen |
1 (* Title: HOL/Tools/float_syntax.ML |
|
2 Author: Tobias Nipkow, TU Muenchen |
2 |
3 |
3 Concrete syntax for floats. |
4 Concrete syntax for floats. |
4 *) |
5 *) |
5 |
6 |
6 signature FLOAT_SYNTAX = |
7 signature FLOAT_SYNTAX = |