[isabelle-dev] Old_Number_Theory

[Manuel Eberl]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20161018/a713d817/attachment.html>