# HG changeset patch
# User nipkow
# Date 1526409286 -7200
# Node ID 695ff8a207b0fd9a1847d0f4fed47666703b0c96
# Parent  6163c90694efaf3676469286747a3383cd83f718
added lemmas

diff -r 6163c90694ef -r 695ff8a207b0 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>