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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
