--- a/src/HOL/HOLCF/Cpo.thy Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Cpo.thy Wed Dec 11 10:40:57 2024 +0100
@@ -558,6 +558,7 @@
end
+
subsection \<open>Discrete cpos\<close>
class discrete_cpo = below +
@@ -799,10 +800,12 @@
apply simp
done
+
section \<open>Admissibility and compactness\<close>
default_sort cpo
+
subsection \<open>Definitions\<close>
definition adm :: "('a::cpo \<Rightarrow> bool) \<Rightarrow> bool"
@@ -969,6 +972,7 @@
adm_below adm_eq adm_not_below
adm_compact_not_below adm_compact_neq adm_neq_compact
+
section \<open>Class instances for the full function space\<close>
subsection \<open>Full function space is a partial order\<close>
@@ -1109,6 +1113,7 @@
for S :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo"
by (simp add: lub_fun ch2ch_lambda)
+
section \<open>The cpo of cartesian products\<close>
subsection \<open>Unit type is a pcpo\<close>
@@ -1401,6 +1406,7 @@
apply (case_tac "\<Squnion>i. Y i", simp)
done
+
section \<open>Discrete cpo types\<close>
datatype 'a discr = Discr "'a :: type"