changeset 35427 | ad039d29e01c |
parent 34941 | 156925dd67af |
child 35783 | 38538bfe9ca6 |
--- a/src/HOLCF/Up.thy Tue Mar 02 23:56:13 2010 +0100 +++ b/src/HOLCF/Up.thy Tue Mar 02 23:59:54 2010 +0100 @@ -14,8 +14,8 @@ datatype 'a u = Ibottom | Iup 'a -syntax (xsymbols) - "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999) +type_notation (xsymbols) + u ("(_\<^sub>\<bottom>)" [1000] 999) primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where "Ifup f Ibottom = \<bottom>"