diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -128,6 +128,7 @@
 apply (erule (1) below_trans)
 done
 
+
 subsection \<open>Lemmas about least upper bounds\<close>
 
 lemma is_ub_thelub_ex: "\<lbrakk>\<exists>u. S <<| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
@@ -184,6 +185,7 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
+
 subsubsection \<open>Principal ideals approximate all elements\<close>
 
 lemma compact_principal [simp]: "compact (principal a)"
@@ -296,6 +298,7 @@
 apply (drule (2) admD2, fast, simp)
 done
 
+
 subsection \<open>Defining functions in terms of basis elements\<close>
 
 definition