| changeset 51542 | 738598beeb26 |
| parent 51375 | d9e62d9c98de |
| child 53215 | 5e47c31c6f7c |
| 51541:e7b6b61b7be2 | 51542:738598beeb26 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Floating-Point Numbers *} |
6 header {* Floating-Point Numbers *} |
7 |
7 |
8 theory Float |
8 theory Float |
9 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" |
9 imports Complex_Main Lattice_Algebras |
10 begin |
10 begin |
11 |
11 |
12 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}" |
12 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}" |
13 |
13 |
14 typedef float = float |
14 typedef float = float |