src/HOL/HOLCF/ConvexPD.thy

--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -466,6 +466,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+
 subsection \<open>Convex powerdomain is bifinite\<close>
 
 lemma approx_chain_convex_map:
@@ -481,6 +482,7 @@
     by (fast intro!: approx_chain_convex_map)
 qed
 
+
 subsection \<open>Join\<close>
 
 definition