Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid theorem name clash (by Jan van Brügge)
authortraytel
Wed, 15 Jan 2025 13:53:25 +0100
changeset 81808 f575ad8dcbe5
parent 81807 cd2521e39783
child 81809 90ee9f9b04de
avoid theorem name clash (by Jan van Brügge)
src/HOL/Cardinals/Wellorder_Constructions.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle