<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">That is great news!<div class=""><br class=""></div><div class="">It’s a pity that our coverage of number theory is minuscule compared with what we have for analysis. I blame John Harrison :-)</div><div class=""><br class=""><div class="">
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 11px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div class="">Larry</div></span>
</div>
<br class=""><div><blockquote type="cite" class=""><div class="">On 18 Oct 2016, at 12:11, Manuel Eberl <<a href="mailto:eberlm@in.tum.de" class="">eberlm@in.tum.de</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="content-type" content="text/html; charset=utf-8" class="">
<div bgcolor="#FFFFFF" text="#000000" class=""><p class=""><font size="+1" class="">I am glad to announce that as of</font><font size="+1" class="">
<meta http-equiv="content-type" content="text/html;
charset=utf-8" class="">
261d42f0bfac, Old_Number_Theory is finally history.</font></p><p class=""><font size="+1" class="">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.</font></p><p class=""><font size="+1" class="">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.<br class="">
</font></p><p class=""><font size="+1" class=""><br class="">
Cheers,</font></p><p class=""><font size="+1" class="">Manuel<br class="">
</font></p>
</div>
_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></blockquote></div><br class=""></div></body></html>