--- a/src/HOL/HOLCF/Lift.thy Wed Dec 11 10:28:12 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy Wed Dec 11 10:40:57 2024 +0100
@@ -19,6 +19,7 @@
Def :: "'a \<Rightarrow> 'a lift" where
"Def x = Abs_lift (up\<cdot>(Discr x))"
+
subsection \<open>Lift as a datatype\<close>
lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
@@ -70,6 +71,7 @@
by (induct x) auto
qed
+
subsection \<open>Continuity of \<^const>\<open>case_lift\<close>\<close>
lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
@@ -82,6 +84,7 @@
"\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
unfolding case_lift_eq by (simp add: cont_Rep_lift)
+
subsection \<open>Further operations\<close>
definition