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 :-)


> On 18 Oct 2016, at 12:11, Manuel Eberl <> 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-dev mailing list

Reply via email to