--- 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