I'm currently cleaning up the Central Limit Theorem, and I want to it
entirely to HOL-Probability.
I hope to finish this in 1 week, to get it into Isabelle 2016.
- Johannes
Am Freitag, den 01.01.2016, 20:24 +0100 schrieb Makarius:
> Isabelle2016-RC0 is published, but we are still in normal
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
I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know
what exactly went wrong or what caused the failure. The problem seems to be related to
some change in theory imports. It seems as if code_pred cannot retrieve the specification
of a constant under certain
