author | wenzelm |
Mon, 23 Oct 2017 20:21:36 +0200 | |
changeset 66907 | 603a00f21817 |
parent 66905 | 0d31dfa96aba (diff) |
parent 66906 | 03a96b8c7c06 (current diff) |
child 66908 | 9b074f01a305 |
--- 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)