diff -r cbc38731d42f -r 8ea7b22525cb src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Mar 04 23:31:04 2015 +0100
@@ -1061,10 +1061,6 @@
     by (auto simp: vimage_def measurable_count_space_eq2_countable)
 qed
 
-lemma measurable_real_natfloor[measurable]:
-  "(natfloor :: real \<Rightarrow> nat) \<in> measurable borel (count_space UNIV)"
-  by (simp add: natfloor_def[abs_def])
-
 lemma measurable_real_ceiling[measurable]:
   "(ceiling :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
   unfolding ceiling_def[abs_def] by simp
@@ -1072,10 +1068,6 @@
 lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   by simp
 
-lemma borel_measurable_real_natfloor:
-  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
-  by simp
-
 lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel"
   by (intro borel_measurable_continuous_on1 continuous_intros)