[isabelle-dev] Old_Number_Theory

[Lawrence Paulson]

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

Larry

> On 18 Oct 2016, at 12:11, Manuel Eberl <eberlm at in.tum.de> 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 at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161018/f2b5823a/attachment-0002.html>