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