One remark on the diff:
+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
This is a formal regression: a proper name has turned into CaMlCaSe.
But that should be easy to correct.
Ah indeed. Jaime probably didn't know about the naming convent
True, but even though I am hardly an expert in number theory, I would
imagine that a solid foundation in analysis (especially complex
analysis) is very helpful, if not indispensable, in the development of
advanced number theory. (the most obvious example is the
complex-analytic proof of PNT and
Hi Manuel,
> I am glad to announce that as of261d42f0bfac, Old_Number_Theory is
> finally history.
these are good news indeed.
One remark on the diff:
+ src/HOL/Number_Theory/QuadraticReciprocity.thy
+ src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
This is a formal regression: a proper na
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 wrote:
>
> I am glad to announce that as of 261d42f0bfac, Old_Number_Theory is finally
> history.
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