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