diff -r 0a01bec9bc13 -r a712bf5ccab0 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Wed Dec 11 10:40:57 2024 +0100
@@ -285,6 +285,7 @@
   "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x"
 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject)
 
+
 subsubsection \<open>Run operator\<close>
 
 definition
@@ -305,6 +306,7 @@
 unfolding run_def succeed_def
 by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
 
+
 subsubsection \<open>Monad plus operator\<close>
 
 definition
@@ -335,6 +337,7 @@
 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)"
 by (cases x, simp_all)
 
+
 subsection \<open>Match functions for built-in types\<close>
 
 default_sort pcpo
@@ -431,6 +434,7 @@
   "match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_FF_def)
 
+
 subsection \<open>Mutual recursion\<close>
 
 text \<open>