Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide



On 22.05.2013 20:10, Brian Huffman wrote:
lemma sorted_list_of_set_distinct [simp] :
   shows "distinct (sorted_list_of_set S)"
apply (cases "finite S")
apply (induct set: finite)
apply (simp_all add: distinct_insort)
done

Only in the development version.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.