[isabelle-dev] Towards the Isabelle2017 release

Manuel Eberl eberlm at in.tum.de
Thu Aug 24 22:39:30 CEST 2017

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)


More information about the isabelle-dev mailing list