--- a/src/HOL/List.thy Sun Nov 04 19:17:13 2007 +0100
+++ b/src/HOL/List.thy Mon Nov 05 08:31:12 2007 +0100
@@ -2581,6 +2581,9 @@
end
+lemma sorted_upt[simp]: "sorted[i..<j]"
+by (induct j) (simp_all add:sorted_append)
+
subsubsection {* @{text sorted_list_of_set} *}