# HG changeset patch
# User wenzelm
# Date 1733909292 -3600
# Node ID 0a01bec9bc1370196681f01cbfabebee6fee421d
# Parent  cb57350beaa908152414867ceb3084a34abb5c7f
clarified default_sort;

diff -r cb57350beaa9 -r 0a01bec9bc13 src/HOL/HOLCF/Cpo.thy
--- 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