src/HOLCF/Up.thy
changeset 26046 1624b3304bb9
parent 26027 87cb69d27558
child 26407 562a1d615336
     1.1 --- a/src/HOLCF/Up.thy	Wed Feb 06 22:10:29 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Thu Feb 07 03:30:32 2008 +0100
     1.3 @@ -233,8 +233,8 @@
     1.4    "fup = (\<Lambda> f p. Ifup f p)"
     1.5  
     1.6  translations
     1.7 -  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
     1.8 -  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
     1.9 +  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    1.10 +  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
    1.11  
    1.12  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    1.13