src/HOL/Real/RComplete.thy
changeset 16827 c90a1f450327
parent 16820 5c9d597e4cb9
child 16893 0cc94e6f6ae5
     1.1 --- a/src/HOL/Real/RComplete.thy	Thu Jul 14 14:05:48 2005 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Thu Jul 14 17:16:52 2005 +0200
     1.3 @@ -354,12 +354,6 @@
     1.4  apply (insert real_lb_ub_int [of r], safe)
     1.5  apply (rule theI2)
     1.6  apply auto
     1.7 -apply (subst int_le_real_less, simp)
     1.8 -apply (drule_tac x = n in spec)
     1.9 -apply auto
    1.10 -apply (subgoal_tac "n <= x")
    1.11 -apply simp
    1.12 -apply (subst int_le_real_less, simp)
    1.13  done
    1.14  
    1.15  lemma floor_mono: "x < y ==> floor x \<le> floor y"
    1.16 @@ -385,7 +379,6 @@
    1.17  apply (insert real_lb_ub_int [of x], erule exE)
    1.18  apply (rule theI2)
    1.19  apply (auto intro: lemma_floor) 
    1.20 -apply (auto simp add: order_eq_iff int_le_real_less)
    1.21  done
    1.22  
    1.23  lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n"
    1.24 @@ -429,7 +422,6 @@
    1.25  apply (insert real_lb_ub_int [of r], safe)
    1.26  apply (rule theI2)
    1.27  apply (auto intro: lemma_floor)
    1.28 -apply (auto simp add: order_eq_iff int_le_real_less)
    1.29  done
    1.30  
    1.31  lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)"
    1.32 @@ -437,7 +429,6 @@
    1.33  apply (insert real_lb_ub_int [of r], safe)
    1.34  apply (rule theI2)
    1.35  apply (auto intro: lemma_floor)
    1.36 -apply (auto simp add: order_eq_iff int_le_real_less)
    1.37  done
    1.38  
    1.39  lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1"