Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed subst step;
authorwenzelm
Sun, 11 Jun 2006 22:45:53 +0200
changeset 19850 29c125556d86
parent 19849 d96a15bb2d88
child 19851 10162c01bd78
fixed subst step;
src/HOL/Real/RComplete.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle