# HG changeset patch
# User huffman
# Date 1315022311 25200
# Node ID 21eb31192850e886be43972b6994454c17ff1563
# Parent  7f0b4515588ac618995fa9fb8779c35d5deb91e5
remove redundant simp rules ceiling_floor and floor_ceiling

diff -r 7f0b4515588a -r 21eb31192850 src/HOL/RComplete.thy
--- 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)