On 2017-08-24 17:34, Florian Haftmann wrote: > I would still appreciate if someone would take the comment »Deviates > from the definition given in the library in number theory« as a starting > point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.
Oh actually I fixed that a few months ago. I even wrote on the mailing list back then, I think. Those definitions should now be equivalent. I didn't know there was a totient function in HOL-Algebra, otherwise I would have removed the duplicate back then. (By the way, I have lots of additional material on the totient function and related functions that will come to an AFP near you very soon) Manuel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
