src/HOLCF/Up.thy
changeset 34941 156925dd67af
parent 33808 31169fdc5ae7
child 35427 ad039d29e01c
     1.1 --- a/src/HOLCF/Up.thy	Sat Jan 16 17:15:27 2010 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Sat Jan 16 17:15:28 2010 +0100
     1.3 @@ -17,12 +17,9 @@
     1.4  syntax (xsymbols)
     1.5    "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
     1.6  
     1.7 -consts
     1.8 -  Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
     1.9 -
    1.10 -primrec
    1.11 -  "Ifup f Ibottom = \<bottom>"
    1.12 -  "Ifup f (Iup x) = f\<cdot>x"
    1.13 +primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
    1.14 +    "Ifup f Ibottom = \<bottom>"
    1.15 + |  "Ifup f (Iup x) = f\<cdot>x"
    1.16  
    1.17  subsection {* Ordering on lifted cpo *}
    1.18