src/HOL/Real/RComplete.thy
changeset 20217 25b068a99d2b
parent 19850 29c125556d86
child 21210 c17fd2df4e9e
     1.1 --- a/src/HOL/Real/RComplete.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -1066,10 +1066,7 @@
     1.4    apply (subgoal_tac "real a = real (int a)")
     1.5    apply (erule ssubst)
     1.6    apply simp
     1.7 -  apply (subst nat_diff_distrib)
     1.8    apply simp
     1.9 -  apply (rule le_floor)
    1.10 -  apply simp_all
    1.11  done
    1.12  
    1.13  lemma natceiling_zero [simp]: "natceiling 0 = 0"
    1.14 @@ -1206,13 +1203,7 @@
    1.15    apply (subgoal_tac "real a = real (int a)")
    1.16    apply (erule ssubst)
    1.17    apply simp
    1.18 -  apply (subst nat_diff_distrib)
    1.19    apply simp
    1.20 -  apply (rule order_trans)
    1.21 -  prefer 2
    1.22 -  apply (rule ceiling_mono2)
    1.23 -  apply assumption
    1.24 -  apply simp_all
    1.25  done
    1.26  
    1.27  lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>