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/Analysis/Path_Connected.thy
changeset 76836 30182f9e1818
parent 74123 7c5842b06114
child 76837 d908a7d3ed1b 
--- a/src/HOL/Analysis/Path_Connected.thy	Sat Dec 31 11:09:19 2022 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun Jan 01 00:45:55 2023 +0000
@@ -2497,7 +2497,7 @@
       by (simp add: inner_commute)
   qed
   obtain S :: "'a set" where "S \<subseteq> Basis" and "card S = Suc (Suc 0)"
-    using ex_card[OF assms]
+    using obtain_subset_with_card_n[OF assms]
     by auto
   then obtain b0 b1 :: 'a where "b0 \<in> Basis" and "b1 \<in> Basis" and "b0 \<noteq> b1"
     unfolding card_Suc_eq by auto
isabelle