# HG changeset patch
# User bulwahn
# Date 1315912672 -7200
# Node ID 8df4c332cb1cc16cd17eb38bc1f3e73a5ad644a4
# Parent  840d8c3d91136e625126b23b0380c2072c2b4c35# Parent  635ae0a736886c084aa20dcc9ac3bb7dad9e75f6
merged

diff -r 635ae0a73688 -r 8df4c332cb1c src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 13 11:24:58 2011 +0200
+++ b/src/HOL/List.thy	Tue Sep 13 13:17:52 2011 +0200
@@ -3867,6 +3867,9 @@
 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
 by (cases xs) auto
 
+lemma sorted_sort_id: "sorted xs \<Longrightarrow> sort xs = xs"
+  by (induct xs) (auto simp add: sorted_Cons insort_is_Cons)
+
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
   by (induct xs) (auto simp add: sorted_Cons)