tuned whitespace

--- a/src/HOL/Wellfounded.thy	Mon Feb 03 10:46:57 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Feb 03 13:04:55 2025 +0100
@@ -395,8 +395,6 @@
 
 subsubsection \<open>Well-foundedness of transitive closure\<close>
 
-
-
 lemma ex_terminating_rtranclp_strong:
   assumes wf: "wfp_on {x'. R\<^sup>*\<^sup>* x x'} R\<inverse>\<inverse>"
   shows "\<exists>y. R\<^sup>*\<^sup>* x y \<and> (\<nexists>z. R y z)"