[isabelle-dev] Towards the release

[Manuel Eberl]

I completed the merge I mentioned in my previous email. Everything went 
into Multivariate_Analysis, apart form Nonpos_Ints and Periodic_Fun, 
which went into Library.

I'm running tests overnight to make sure I did not break anything.

Manuel


On 01/01/16 20:50, Manuel Eberl wrote:
> 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
>>