Re: [isabelle] remdups_adj crucial lemma
Important lemma. I have just added a more succinct proof of it due to Manuel
Eberl http://shodan.linuxd.org/paste/oyIsOBq1 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and