src/HOL/List.thy

--- a/src/HOL/List.thy	Tue May 15 13:57:39 2018 +0200
+++ b/src/HOL/List.thy	Tue May 15 20:34:46 2018 +0200
@@ -5190,6 +5190,12 @@
 
 end
 
+lemma sorted_upt[simp]: "sorted [m..<n]"
+by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upt])
+
+lemma sorted_upto[simp]: "sorted [m..n]"
+by(simp add: sorted_sorted_wrt sorted_wrt_mono_rel[OF _ sorted_wrt_upto])
+
 
 subsubsection \<open>Sorting functions\<close>