Am 24.08.2017 um 22:39 schrieb Manuel Eberl:
> 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.

This sound good.

> I didn't know there was a totient function in HOL-Algebra, otherwise I
> would have removed the duplicate back then.

I had a look at it; I think to reconcile it we would have to move
Totient.thy to Library/, otherwise there would be a dependency cycle.

Looks like something to be done not before the next release.

Cheers,
        Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to