# HG changeset patch
# User desharna
# Date 1738584295 -3600
# Node ID 46b21e6b64b24a18f7dd21af39cf4ba1060a0e4b
# Parent  ba32209092213c33523db9860a53de75ff5088e4
tuned whitespace

diff -r ba3220909221 -r 46b21e6b64b2 src/HOL/Wellfounded.thy
--- 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)"