--- a/src/HOL/Library/Float.thy Wed Nov 11 18:32:26 2015 +0100
+++ b/src/HOL/Library/Float.thy Wed Nov 11 18:32:36 2015 +0100
@@ -31,7 +31,6 @@
declare real_of_float_inverse[simp] float_of_inverse [simp]
declare real_of_float [simp]
-
subsection \<open>Real operations preserving the representation as floating point number\<close>
lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
@@ -214,6 +213,12 @@
end
+lemma real_of_float [simp]: "real_of_float (of_nat n) = of_nat n"
+by (induct n) simp_all
+
+lemma real_of_float_of_int_eq [simp]: "real_of_float (of_int z) = of_int z"
+ by (cases z rule: int_diff_cases) (simp_all add: of_rat_diff)
+
lemma Float_0_eq_0[simp]: "Float 0 e = 0"
by transfer simp