changeset 58889 | 5b7a9633cfa8 |
parent 56255 | 968667bbb8d2 |
child 60017 | b785d6d06430 |
58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
---|---|
1 (* Title: HOL/Matrix_LP/ComputeFloat.thy |
1 (* Title: HOL/Matrix_LP/ComputeFloat.thy |
2 Author: Steven Obua |
2 Author: Steven Obua |
3 *) |
3 *) |
4 |
4 |
5 header {* Floating Point Representation of the Reals *} |
5 section {* Floating Point Representation of the Reals *} |
6 |
6 |
7 theory ComputeFloat |
7 theory ComputeFloat |
8 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" |
8 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras" |
9 begin |
9 begin |
10 |
10 |