diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Compact_Basis.thy
--- 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