src/HOLCF/Up.thy
changeset 18078 20e5a6440790
parent 17838 3032e90c4975
child 18290 5fc309770840
     1.1 --- a/src/HOLCF/Up.thy	Thu Nov 03 01:02:29 2005 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Nov 03 01:11:39 2005 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4  apply (rule_tac j="j" in is_lub_range_shift [THEN iffD1, standard])
     1.5  apply (erule monofun_Ifup2 [THEN ch2ch_monofun])
     1.6  apply (simp add: cont_cfun_arg)
     1.7 -apply (simp add: thelub_const lub_const)
     1.8 +apply (simp add: lub_const)
     1.9  done
    1.10  
    1.11  subsection {* Continuous versions of constants *}
    1.12 @@ -202,7 +202,8 @@
    1.13    "fup \<equiv> \<Lambda> f p. Ifup f p"
    1.14  
    1.15  translations
    1.16 -  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(LAM x. t)\<cdot>l"
    1.17 +  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    1.18 +  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
    1.19  
    1.20  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    1.21  
    1.22 @@ -248,7 +249,7 @@
    1.23  apply (erule (1) admD)
    1.24  apply (rule allI, drule_tac x="i + j" in spec)
    1.25  apply simp
    1.26 -apply (simp add: thelub_const)
    1.27 +apply simp
    1.28  done
    1.29  
    1.30  text {* properties of fup *}