--- a/src/HOL/HOLCF/Compact_Basis.thy Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Wed Dec 11 10:40:57 2024 +0100
@@ -10,6 +10,7 @@
default_sort bifinite
+
subsection \<open>A compact basis for powerdomains\<close>
definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
@@ -40,6 +41,7 @@
(* FIXME: why doesn't ".." or "by (rule exI)" work? *)
qed
+
subsection \<open>Unit and plus constructors\<close>
definition
@@ -91,6 +93,7 @@
apply (rule PDUnit, erule PDPlus [OF PDUnit])
done
+
subsection \<open>Fold operator\<close>
definition