--- a/src/HOL/HOLCF/Bifinite.thy Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
default_sort cpo
+
subsection \<open>Chains of finite deflations\<close>
locale approx_chain =
@@ -43,6 +44,7 @@
end
+
subsection \<open>Omega-profinite and bifinite domains\<close>
class bifinite = pcpo +
@@ -51,6 +53,7 @@
class profinite = cpo +
assumes profinite: "\<exists>(a::nat \<Rightarrow> 'a\<^sub>\<bottom> \<rightarrow> 'a\<^sub>\<bottom>). approx_chain a"
+
subsection \<open>Building approx chains\<close>
lemma approx_chain_iso:
@@ -155,6 +158,7 @@
using chain_discr_approx lub_discr_approx finite_deflation_discr_approx
by (rule approx_chain.intro)
+
subsection \<open>Class instance proofs\<close>
instance bifinite \<subseteq> profinite