src/HOLCF/Up.thy
 changeset 25131 2c8caac48ade parent 19105 3aabd46340e0 child 25785 dbe118fe3180
```     1.1 --- a/src/HOLCF/Up.thy	Sun Oct 21 14:21:45 2007 +0200
1.2 +++ b/src/HOLCF/Up.thy	Sun Oct 21 14:21:48 2007 +0200
1.3 @@ -115,7 +115,7 @@
1.4  by (rule ext, rule up_lemma3 [symmetric])
1.5
1.6  lemma up_lemma6:
1.7 -  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
1.8 +  "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>
1.9        \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
1.10  apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
1.11  apply assumption
1.12 @@ -197,16 +197,17 @@
1.13
1.14  subsection {* Continuous versions of constants *}
1.15
1.16 -constdefs
1.17 -  up  :: "'a \<rightarrow> 'a u"
1.18 -  "up \<equiv> \<Lambda> x. Iup x"
1.19 +definition
1.20 +  up  :: "'a \<rightarrow> 'a u" where
1.21 +  "up = (\<Lambda> x. Iup x)"
1.22
1.23 -  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b"
1.24 -  "fup \<equiv> \<Lambda> f p. Ifup f p"
1.25 +definition
1.26 +  fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where
1.27 +  "fup = (\<Lambda> f p. Ifup f p)"
1.28
1.29  translations
1.30 -  "case l of up\<cdot>x \<Rightarrow> t" == "fup\<cdot>(\<Lambda> x. t)\<cdot>l"
1.31 -  "\<Lambda>(up\<cdot>x). t" == "fup\<cdot>(\<Lambda> x. t)"
1.32 +  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
1.33 +  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
1.34
1.35  text {* continuous versions of lemmas for @{typ "('a)u"} *}
1.36
```