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