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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
