remove redundant simp rules ceiling_floor and floor_ceiling

--- a/src/HOL/RComplete.thy	Fri Sep 02 16:58:00 2011 -0700
+++ b/src/HOL/RComplete.thy	Fri Sep 02 20:58:31 2011 -0700
@@ -255,12 +255,6 @@
 lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n"
   unfolding real_of_nat_def by simp
 
-lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r"
-  unfolding real_of_int_def by simp
-
-lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r"
-  unfolding real_of_int_def by simp
-
 lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)"
   unfolding real_of_int_def by (rule le_of_int_ceiling)