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