# HG changeset patch
# User nipkow
# Date 1508762710 -7200
# Node ID 0d31dfa96abafe8c50a6ad3bb4234a9104f50435
# Parent  d9783ea1160c530a7fda22051a7856aa33c15211
added lemma

diff -r d9783ea1160c -r 0d31dfa96aba src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 23 14:12:09 2017 +0200
+++ b/src/HOL/List.thy	Mon Oct 23 14:45:10 2017 +0200
@@ -5022,6 +5022,9 @@
   with \<open>sorted xs\<close> show ?thesis by (simp add: sorted_append)
 qed
 
+lemma sorted_replicate [simp]: "sorted(replicate n x)"
+by(induction n) (auto simp: sorted_Cons)
+
 lemma sorted_remdups[simp]:
   "sorted l \<Longrightarrow> sorted (remdups l)"
 by (induct l) (auto simp: sorted_Cons)