| changeset 29988 | 747f0c519090 |
| parent 29804 | e15b74577368 |
| child 30034 | 60f64f112174 |
| 29987:391dcbd7e4dd | 29988:747f0c519090 |
|---|---|
1 (* Title: HOL/Library/Float.thy |
1 (* Title: HOL/Library/Float.thy |
2 * Author: Steven Obua 2008 |
2 * Author: Steven Obua 2008 |
3 * Johannes Hölzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 |
3 * Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 |
4 *) |
4 *) |
5 |
|
6 header {* Floating-Point Numbers *} |
|
7 |
|
5 theory Float |
8 theory Float |
6 imports Complex_Main |
9 imports Complex_Main |
7 begin |
10 begin |
8 |
11 |
9 definition |
12 definition |