# HG changeset patch
# User paulson
# Date 1523635257 -3600
# Node ID 06bce659d41bdbe05f5ec799f32969d347c12931
# Parent  9ecc78bcf1efa72c17408640efb6de213b8ad02f# Parent  557ea2740125b35d5fbcf6cc4ad7419134b789f1
merged

diff -r 557ea2740125 -r 06bce659d41b src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Apr 13 15:58:27 2018 +0100
+++ b/src/HOL/List.thy	Fri Apr 13 17:00:57 2018 +0100
@@ -4962,6 +4962,9 @@
   "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
 by(induction xs rule: induct_list012)(auto)
 
+lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
+by(auto simp: le_Suc_eq length_Suc_conv)
+
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
 lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [0..<n]"