[isabelle-dev] NEWS: HOL-Probability -- type of emeasure and nn_integral was changed from ereal to ennreal

[Johannes Hölzl]

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.

 - Johannes



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
> INCOMPATIBILITY.
> 
> 
> 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