Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemmas
authornipkow
Tue, 15 May 2018 20:34:46 +0200
changeset 68190 695ff8a207b0
parent 68189 6163c90694ef
child 68191 4ac04fe61e98
added lemmas
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle