Re: [isabelle-dev] Distro broken

2016-10-18 Thread Johannes Hölzl
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-dev] Distro broken

2016-10-18 Thread Florian Haftmann
> 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 >

Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Manuel Eberl
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

Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Manuel Eberl
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

Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread Florian Haftmann
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

Re: [isabelle-dev] Old_Number_Theory

2016-10-18 Thread 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 wrote: > > I am glad to announce that as of 261d42f0bfac, Old_Number_Theory is

[isabelle-dev] Old_Number_Theory

2016-10-18 Thread Manuel Eberl
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