src/HOL/Library/Equipollence.thy

--- a/src/HOL/Library/Equipollence.thy	Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Library/Equipollence.thy	Tue Jan 31 14:05:16 2023 +0000
@@ -186,7 +186,7 @@
 
 lemma lesspoll_Pow_self: "A \<prec> Pow A"
   unfolding lesspoll_def bij_betw_def eqpoll_def
-  by (meson lepoll_Pow_self Cantors_paradox)
+  by (meson lepoll_Pow_self Cantors_theorem)
 
 lemma finite_lesspoll_infinite:
   assumes "infinite A" "finite B" shows "B \<prec> A"