src/HOLCF/Up.thy
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>"