# HG changeset patch
# User haftmann
# Date 1751788892 -7200
# Node ID 71cbfcda66d6df63084fd2f07a0b3911e70879ef
# Parent  638c73041d96722265fd42b286f6602885d3450e
more correct lemma name

diff -r 638c73041d96 -r 71cbfcda66d6 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jul 08 14:42:35 2025 +0200
+++ b/src/HOL/List.thy	Sun Jul 06 10:01:32 2025 +0200
@@ -8510,7 +8510,7 @@
 qualified definition Least :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
   where Least_eq [code_abbrev, simp]: \<open>Least S = (LEAST x. x \<in> S)\<close>
 
-qualified lemma Min_filter_eq [code_abbrev]:
+qualified lemma Least_filter_eq [code_abbrev]:
   \<open>Least (Set.filter P S) = (LEAST x. x \<in> S \<and> P x)\<close>
   by simp