Re: [isabelle] Reindexing series

Dear Johannes and Joachim,

Thanks a lot for your efforts. I'll generalise and polish Joachim's proof a bit and ultimately will add it to the repository. I won't try to abstract from reals to some type class because both of your proofs rely on lemmas about the reals.


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