# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1672537382 0
# Node ID d908a7d3ed1b298234b84326dc5460e1fe01a7c0
# Parent  30182f9e1818c220110389775eb4f5de35789da7
A couple of patches

diff -r 30182f9e1818 -r d908a7d3ed1b src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Sun Jan 01 00:45:55 2023 +0000
+++ b/src/HOL/Analysis/Determinants.thy	Sun Jan 01 01:43:02 2023 +0000
@@ -1026,7 +1026,7 @@
       using \<open>A *v axis k 1 = a\<close> that by auto
   next
     from obtain_subset_with_card_n[OF 2] obtain h i::'n where "h \<noteq> i"
-      by (auto simp add: eval_nat_numeral card_Suc_eq)
+      by (fastforce simp add: eval_nat_numeral card_Suc_eq)
     then obtain j where "j \<noteq> k"
       by (metis (full_types))
     let ?TA = "transpose A"
diff -r 30182f9e1818 -r d908a7d3ed1b src/HOL/Analysis/Path_Connected.thy
--- 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"