# 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)