changeset 41959 | b460124855b8 |
parent 41550 | efa734d9b221 |
child 42676 | 8724f20bf69c |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: HOL/Tools/ComputeFloat.thy |
1 (* Title: HOL/Matrix/ComputeFloat.thy |
2 Author: Steven Obua |
2 Author: Steven Obua |
3 *) |
3 *) |
4 |
4 |
5 header {* Floating Point Representation of the Reals *} |
5 header {* Floating Point Representation of the Reals *} |
6 |
6 |
7 theory ComputeFloat |
7 theory ComputeFloat |