Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Cardinals/Wellorder_Constructions.thy
changeset 81808 f575ad8dcbe5
parent 80067 c40bdfc84640
child 82248 e8c96013ea8a 
--- 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