eberlm at in.tum.de
Tue Oct 18 13:11:46 CEST 2016
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev