src/HOLCF/Up.thy
changeset 25922 cb04d05e95fb
parent 25921 0ca392ab7f37
child 26027 87cb69d27558
     1.1 --- a/src/HOLCF/Up.thy	Thu Jan 17 00:51:20 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Jan 17 21:44:19 2008 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  lemma up_lemma2:
     1.5    "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
     1.6  apply (erule contrapos_nn)
     1.7 -apply (drule_tac x="j" and y="i + j" in chain_mono3)
     1.8 +apply (drule_tac i="j" and j="i + j" in chain_mono)
     1.9  apply (rule le_add2)
    1.10  apply (case_tac "Y j")
    1.11  apply assumption