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/Library/Multiset_Order.thy
changeset 79669 a3e7a323780f
parent 78099 4d9349989d94
child 79800 abb5e57c92a7 
--- 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)
isabelle