equal
deleted
inserted
replaced
2 |
2 |
3 theory Code_Real_Approx_By_Float |
3 theory Code_Real_Approx_By_Float |
4 imports Complex_Main 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\<open>\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) |
10 disproved by mapping it to machine reals. |
10 disproved by mapping it to machine reals. |
11 |
11 |
12 The value command cannot display real results yet. |
12 The value command cannot display real results yet. |
13 |
13 |
14 The only legitimate use of this theory is as a tool for code generation |
14 The only legitimate use of this theory is as a tool for code generation |
15 purposes. *} |
15 purposes.\<close> |
16 |
16 |
17 code_printing |
17 code_printing |
18 type_constructor real \<rightharpoonup> |
18 type_constructor real \<rightharpoonup> |
19 (SML) "real" |
19 (SML) "real" |
20 and (OCaml) "float" |
20 and (OCaml) "float" |