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