--- a/src/HOL/HOLCF/Deflation.thy Wed Dec 11 10:28:12 2024 +0100 +++ b/src/HOL/HOLCF/Deflation.thy Wed Dec 11 10:40:57 2024 +0100 @@ -313,6 +313,7 @@ end + subsection \<open>Uniqueness of ep-pairs\<close> lemma ep_pair_unique_e_lemma: