[isabelle-dev] Towards the release

[Manuel Eberl]

I still have a few thousand lines of stuff to merge into the 
distribution, most notably the definition of the radius of convergence 
of a series and a number of convergence tests.

This would be nice to have in the distribution because two results of 
mathematical importance rest upon it: the Gamma function and the 
Generalised Binomial Theorem.

The work itself is already, all that remains is to merge it into the 
distribution. I put the files in this repository if anyone wants to look 
at them: https://github.com/3of8/isabelle_summation

The only files that require any real merging (as opposed to just copying 
the file into the distribution) are Summation.thy, 
Extended_Real_Lemma_Bucket.thy, and Liminf_Limsup_Lemma_Bucket.thy. The 
file "Concave.thy" is not required by the rest and does not need to be 
merged.


None of this really has to end up in Isabelle2016; I can also wait for 
the next release. My plan was to meet with Johannes and Fabian after the 
holidays and ask them for their opinions on this material.


Cheers,

Manuel


On 01/01/16 20:24, Makarius wrote:
> Isabelle2016-RC0 is published, but we are still in normal incremental
> change mode on the isabelle-dev repository.
>
> This is also an opportunity to check NEWS, ANNOUNCE, CONTRIBUTORS, and
> the website.
>
>
> Are there bigger changes still in the pipeline?  Larry are you finished
> with the ports from HOL Light, as far as Isabelle2016 is concerned?
>
> Depending on that, the fork point for the release will be a bit sooner
> or later.  Lets say in about 2 weeks. Hopefully, Oracle manages to
> deliver the next Java 8 update in 3 weeks, as scheduled.
>
>
>      Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev