I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
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.
isabelle-dev mailing list