Re: [isabelle] remdups_adj crucial lemma

Important lemma. I have just added a more succinct proof of it due to Manuel
Eberl to List.thy.

Thanks to both of you!

On 23/08/2014 12:19, Jakob von Raumer wrote:
> Hello everyone,
> am I just bad at using find_theorems or is there no lemma that remdups_adj
> really yields lists with no adjacent entries being equal? If it's really
> missing, here's my somewhat lengthy proof:
> Best regards
> Jakob

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