I am glad to announce that as of261d42f0bfac, 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
