[isabelle-dev] Towards the release

Manuel Eberl eberlm at in.tum.de
Fri Jan 1 20:50:22 CET 2016

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 

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.



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

More information about the isabelle-dev mailing list