# HG changeset patch
# User nipkow
# Date 1667893289 -3600
# Node ID a125c8baf643bb04a37f447e34811d3308798d36
# Parent  defaa0b1742433130d2150e8ca5cdf14b9a93452
retain derived lemma for better findability

diff -r defaa0b17424 -r a125c8baf643 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 07 22:16:37 2022 +0100
+++ b/src/HOL/List.thy	Tue Nov 08 08:41:29 2022 +0100
@@ -5882,7 +5882,11 @@
 by (cases xs) auto
 
 lemma sort_key_id_if_sorted: "sorted (map f xs) \<Longrightarrow> sort_key f xs = xs"
-by (induct xs) (auto simp add: insort_is_Cons)
+by (induction xs) (auto simp add: insort_is_Cons)
+
+text \<open>Subsumed by @{thm sort_key_id_if_sorted} but easier to find:\<close>
+lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+by (simp add: sort_key_id_if_sorted)
 
 lemma insort_key_remove1:
   assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"