diff -r 878f37493934 -r 32dd31062eaa src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jun 13 17:16:53 2025 +0200
+++ b/src/HOL/List.thy	Fri Jun 13 20:59:51 2025 +0200
@@ -4740,7 +4740,7 @@
 
 text \<open>Conceptually, the result of \<^const>\<open>minus_list_set\<close> is only determined up to the set of elements:\<close>
 
-lemma set_minus_list_set: "set(minus_list_set xs ys) = set xs - set ys"
+lemma set_minus_list_set[simp]: "set(minus_list_set xs ys) = set xs - set ys"
 by(induction ys) (auto simp: minus_list_set_def)
 
 lemma minus_list_set_Nil2[simp]: "minus_list_set xs [] = xs"