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 76837 d908a7d3ed1b
parent 76836 30182f9e1818
child 76874 d6b02d54dbf8 
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Jan 01 00:45:55 2023 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy	Sun Jan 01 01:43:02 2023 +0000
@@ -2497,8 +2497,7 @@
       by (simp add: inner_commute)
   qed
   obtain S :: "'a set" where "S \<subseteq> Basis" and "card S = Suc (Suc 0)"
-    using obtain_subset_with_card_n[OF assms]
-    by auto
+    using obtain_subset_with_card_n[OF assms] by (force simp add: eval_nat_numeral)
   then obtain b0 b1 :: 'a where "b0 \<in> Basis" and "b1 \<in> Basis" and "b0 \<noteq> b1"
     unfolding card_Suc_eq by auto
   then have "a + b0 - b1 \<in> ?A \<inter> ?B"
isabelle