src/HOL/HOLCF/LowerPD.thy

--- a/src/HOL/HOLCF/LowerPD.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -459,6 +459,7 @@
     by (rule finite_range_imp_finite_fixes)
 qed
 
+
 subsection \<open>Lower powerdomain is bifinite\<close>
 
 lemma approx_chain_lower_map:
@@ -474,6 +475,7 @@
     by (fast intro!: approx_chain_lower_map)
 qed
 
+
 subsection \<open>Join\<close>
 
 definition