equal
deleted
inserted
replaced
12 |
12 |
13 subsection {* Definition of new type for lifting *} |
13 subsection {* Definition of new type for lifting *} |
14 |
14 |
15 datatype 'a u = Ibottom | Iup 'a |
15 datatype 'a u = Ibottom | Iup 'a |
16 |
16 |
17 syntax (xsymbols) |
17 type_notation (xsymbols) |
18 "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999) |
18 u ("(_\<^sub>\<bottom>)" [1000] 999) |
19 |
19 |
20 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where |
20 primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where |
21 "Ifup f Ibottom = \<bottom>" |
21 "Ifup f Ibottom = \<bottom>" |
22 | "Ifup f (Iup x) = f\<cdot>x" |
22 | "Ifup f (Iup x) = f\<cdot>x" |
23 |
23 |