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!
Tobias

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:
> https://gist.github.com/javra/68c7f852a060d7cb6036
> 
> Best regards
> Jakob
> 




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