# HG changeset patch
# User wenzelm
# Date 1508782896 -7200
# Node ID 603a00f21817b3080a890443a786ce15ce023764
# Parent  0d31dfa96abafe8c50a6ad3bb4234a9104f50435# Parent  03a96b8c7c0641f88d3b8262c7d2735f044a4ca5
merged

diff -r 03a96b8c7c06 -r 603a00f21817 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 23 19:30:39 2017 +0200
+++ b/src/HOL/List.thy	Mon Oct 23 20:21:36 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)