# HG changeset patch # User wenzelm # Date 1150058753 -7200 # Node ID 29c125556d868fdaf194ba69c6f23898a7d8993d # Parent d96a15bb2d88503239621a8211c71e2f81fbb5ee fixed subst step; diff -r d96a15bb2d88 -r 29c125556d86 src/HOL/Real/RComplete.thy --- a/src/HOL/Real/RComplete.thy Sun Jun 11 21:59:30 2006 +0200 +++ b/src/HOL/Real/RComplete.thy Sun Jun 11 22:45:53 2006 +0200 @@ -1159,7 +1159,7 @@ lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" apply (unfold natceiling_def) - apply (subst nat_int [THEN sym]);back; + apply (simplesubst nat_int [THEN sym]) back back apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") apply (erule ssubst) apply (subst eq_nat_nat_iff)