author | immler |
Fri, 26 Feb 2016 11:53:42 +0100 | |
changeset 62419 | c7d6f4dded19 |
parent 62418 | f1b0908028cf |
child 62420 | c7666166c24e |
--- a/src/HOL/Library/Float.thy Thu Feb 25 20:35:05 2016 +0100 +++ b/src/HOL/Library/Float.thy Fri Feb 26 11:53:42 2016 +0100 @@ -171,12 +171,12 @@ by simp declare Float.rep_eq[simp] +code_datatype Float + lemma compute_real_of_float[code]: "real_of_float (Float m e) = (if e \<ge> 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))" by (simp add: powr_int) -code_datatype Float - subsection \<open>Arithmetic operations on floating point numbers\<close>