That is great news! It’s a pity that our coverage of number theory is minuscule compared with what we have for analysis. I blame John Harrison :-)
Larry > On 18 Oct 2016, at 12:11, Manuel Eberl <ebe...@in.tum.de> wrote: > > I am glad to announce that as of 261d42f0bfac, Old_Number_Theory is finally > history. > > A lot of the proofs are still quite messy and don't take advantage of the new > features we now have in Number_Theory (such as a uniform concept of ‘primes’ > and ‘prime factorisations’ for both nat and int), but I do not think the work > necessary to achieve that is worth it. > > The vast majority of the porting work was done by a student of ours, Jaime > Mendizabal Roche, so big thanks to him. He even extended the ‘two squares’ > AFP entry a bit, showing the converse direction as well. > > > Cheers, > > Manuel > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
