My bad, should be fixed now.
- Jo
Am Dienstag, den 18.10.2016, 20:40 +0200 schrieb Florian Haftmann:
> >
> > isabelle: fb5c74a58796 tip
> > afp: c03838321f2a tip
> > *** No such file:
> > "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Ess
> > ential_Supremum.thy"
> > *** The
> isabelle: fb5c74a58796 tip
> afp: c03838321f2a tip
> *** No such file:
> "/mnt/home/haftmann/data/tum/isabelle/devel/src/HOL/Probability/Essential_Supremum.thy"
> *** The error(s) above occurred for theory "Essential_Supremum"
> *** (required by "Probability") (line 15 of
>
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
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
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
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
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