[isabelle-dev] duplicate fact in List

[Tobias Nipkow]

Thanks, have renamed both to Cons_nth_drop_Suc.

Tobias

On 09/09/2014 15:33, Christian Sternagel wrote:
> Dear all,
> 
> just an observation. The facts
> 
>   List.drop_Suc_conv_tl:
>     ?i < length ?xs ⟹
>     ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
>   List.nth_drop':
>     ?i < length ?xs ⟹
>     ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
> 
> are duplicates of each other.
> 
> cheers
> 
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev