[isabelle-dev] NEWS: HOL-Probability -- type of emeasure and nn_integral was changed from ereal to ennreal
hoelzl at in.tum.de
Fri Apr 15 10:20:48 CEST 2016
Argh, the change to the AFP broke the entire build by accidentally
removing `Ergodic_Theory/document/root.tex`. I don't know how this
happened. It is fixed now. Sorry for the inconvenience.
Am Donnerstag, den 14.04.2016, 15:57 +0200 schrieb Johannes Hölzl:
> In HOL-Probability the type of emeasure and nn_integral was changed
> from ereal to ennreal:
> emeasure :: 'a measure => 'a set => ennreal
> nn_integral :: 'a measure => ('a => ennreal) => ennreal
> This is a major incompatibility for most users of HOL-Probability. I
> changed the Isabelle repository and the AFP. I hope there are not too
> many external theories.
> - Johannes
More information about the isabelle-dev