equal
deleted
inserted
replaced
1 (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *) |
1 (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *) |
2 |
2 |
3 theory Code_Real_Approx_By_Float |
3 theory Code_Real_Approx_By_Float |
4 imports Complex_Main "~~/src/HOL/Library/Code_Target_Int" |
4 imports Complex_Main Code_Target_Int |
5 begin |
5 begin |
6 |
6 |
7 text{* \textbf{WARNING} This theory implements mathematical reals by machine |
7 text{* \textbf{WARNING} This theory implements mathematical reals by machine |
8 reals (floats). This is inconsistent. See the proof of False at the end of |
8 reals (floats). This is inconsistent. See the proof of False at the end of |
9 the theory, where an equality on mathematical reals is (incorrectly) |
9 the theory, where an equality on mathematical reals is (incorrectly) |