src/HOL/List.thy

 apply (auto simp: sorted_distinct_set_unique)
 done
 
 end
 
+lemma sorted_upt[simp]: "sorted[i..<j]"
+by (induct j) (simp_all add:sorted_append)
+
 
 subsubsection {* @{text sorted_list_of_set} *}
 
 text{* This function maps (finite) linearly ordered sets to sorted
 lists. Warning: in most cases it is not a good idea to convert from