src/HOLCF/Up.thy
changeset 17585 f12d7ac88eb4
parent 16933 91ded127f5f7
child 17838 3032e90c4975
     1.1 --- a/src/HOLCF/Up.thy	Thu Sep 22 18:59:41 2005 +0200
     1.2 +++ b/src/HOLCF/Up.thy	Thu Sep 22 19:06:05 2005 +0200
     1.3 @@ -130,9 +130,7 @@
     1.4  apply (simp add: expand_fun_eq)
     1.5  apply (erule exE, rename_tac j)
     1.6  apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
     1.7 -apply (rule conjI)
     1.8  apply (simp add: up_lemma4)
     1.9 -apply (rule conjI)
    1.10  apply (simp add: up_lemma6 [THEN thelubI])
    1.11  apply (rule_tac x=j in exI)
    1.12  apply (simp add: up_lemma3)
    1.13 @@ -143,8 +141,7 @@
    1.14  apply (rule_tac x="Iup (lub (range A))" in exI)
    1.15  apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
    1.16  apply (simp add: is_lub_Iup thelubE)
    1.17 -apply (rule_tac x="Ibottom" in exI)
    1.18 -apply (rule lub_const)
    1.19 +apply (rule exI, rule lub_const)
    1.20  done
    1.21  
    1.22  instance u :: (cpo) cpo
    1.23 @@ -152,7 +149,7 @@
    1.24  
    1.25  subsection {* Type @{typ "'a u"} is pointed *}
    1.26  
    1.27 -lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
    1.28 +lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
    1.29  apply (rule_tac x = "Ibottom" in exI)
    1.30  apply (rule minimal_up [THEN allI])
    1.31  done