[isabelle-dev] Towards the release
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev