# HG changeset patch
# User traytel
# Date 1736945605 -3600
# Node ID f575ad8dcbe5b2690d53827747a843555446c025
# Parent  cd2521e39783fd719be53f2468b9f46a54b48c00
avoid theorem name clash (by Jan van Brügge)

diff -r cd2521e39783 -r f575ad8dcbe5 src/HOL/Cardinals/Wellorder_Constructions.thy
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Wed Jan 15 13:53:03 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Wed Jan 15 13:53:25 2025 +0100
@@ -322,7 +322,7 @@
   shows "P a"
   by (induct rule: well_order_induct) (rule assms, simp add: underS_def)
 
-lemma suc_underS:
+lemma suc_underS':
   assumes B: "B \<subseteq> Field r" and A: "AboveS B \<noteq> {}" and b: "b \<in> B"
   shows "b \<in> underS (suc B)"
   using suc_AboveS[OF B A] b unfolding underS_def AboveS_def by auto