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