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