Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Up.thy
changeset 16933 91ded127f5f7
parent 16753 fb6801c926d2
child 17585 f12d7ac88eb4 
--- a/src/HOLCF/Up.thy	Thu Jul 28 15:19:47 2005 +0200
+++ b/src/HOLCF/Up.thy	Thu Jul 28 15:19:48 2005 +0200
@@ -114,7 +114,7 @@
 lemma up_lemma6:
   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
       \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
-apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
+apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
 apply assumption
 apply (subst up_lemma5, assumption+)
 apply (rule is_lub_Iup)
isabelle