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