changeset 81583 | b6df83045178 |
parent 81095 | 49c04500c5f9 |
--- a/src/HOL/HOLCF/Up.thy Thu Dec 12 12:35:59 2024 +0100 +++ b/src/HOL/HOLCF/Up.thy Thu Dec 12 15:45:29 2024 +0100 @@ -9,9 +9,6 @@ imports Cfun begin -default_sort cpo - - subsection \<open>Definition of new type for lifting\<close> datatype 'a u (\<open>(\<open>notation=\<open>postfix lifting\<close>\<close>_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a