# HG changeset patch
# User blanchet
# Date 1708349486 -3600
# Node ID a3e7a323780f6b3cc3b3da8455e85e7d7fcdb694
# Parent  9f36a31fe7ae86fc3e6e42b252383325474b899f
remove selected occurrences of 'moura' tactic

diff -r 9f36a31fe7ae -r a3e7a323780f src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Mon Feb 19 11:39:00 2024 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Mon Feb 19 14:31:26 2024 +0100
@@ -1178,7 +1178,7 @@
       if "openin (top_of_set U) V" "T retract_of V" "U \<noteq> {}" for V
     using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
   obtain Ta where "(openin (top_of_set U) Ta \<and> T retract_of Ta)"
-    using ANR_def UT \<open>S homeomorphic T\<close> assms by moura
+    using ANR_def UT \<open>S homeomorphic T\<close> assms by atomize_elim (auto simp: choice)
   then show ?thesis
     using S \<open>U \<noteq> {}\<close> by blast
 qed
diff -r 9f36a31fe7ae -r a3e7a323780f src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Feb 19 11:39:00 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 19 14:31:26 2024 +0100
@@ -652,7 +652,7 @@
       by (metis image_mset_Diff image_mset_union)
   next
     obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
-      using ex_y by moura
+      using ex_y by metis
 
     show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
     proof (intro allI impI)