src/HOL/Real/RComplete.thy
changeset 19850 29c125556d86
parent 19765 dfe940911617
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Real/RComplete.thy	Sun Jun 11 21:59:30 2006 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Sun Jun 11 22:45:53 2006 +0200
     1.3 @@ -1159,7 +1159,7 @@
     1.4  
     1.5  lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1"
     1.6    apply (unfold natceiling_def)
     1.7 -  apply (subst nat_int [THEN sym]);back;
     1.8 +  apply (simplesubst nat_int [THEN sym]) back back
     1.9    apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)")
    1.10    apply (erule ssubst)
    1.11    apply (subst eq_nat_nat_iff)