--- a/src/HOL/HOLCF/Cpo.thy Tue Dec 10 22:59:13 2024 +0100
+++ b/src/HOL/HOLCF/Cpo.thy Wed Dec 11 10:28:12 2024 +0100
@@ -595,16 +595,9 @@
section \<open>Continuity and monotonicity\<close>
-text \<open>
- Now we change the default class! Form now on all untyped type variables are
- of default class po
-\<close>
-
-default_sort po
-
subsection \<open>Definitions\<close>
-definition monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" \<comment> \<open>monotonicity\<close>
+definition monofun :: "('a::po \<Rightarrow> 'b::po) \<Rightarrow> bool" \<comment> \<open>monotonicity\<close>
where "monofun f \<longleftrightarrow> (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
definition cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
@@ -1118,9 +1111,6 @@
section \<open>The cpo of cartesian products\<close>
-default_sort cpo
-
-
subsection \<open>Unit type is a pcpo\<close>
instantiation unit :: discrete_cpo