Unfortunately it is not easily upgraded, as I did a semantic change in
HOL-Probability (i.e. ereal -> ennreal).
My local version of MFMC is currently 25% ported, and I hope to be
finished in a couple of days. (I didn't work on it over the long
weekend)
- Johannes
On Mo, 2016-05-30 at 23:28
As of Isabelle/dd6cd88cebd9 + AFP/8186added238, MFMC_Countable is still
failing.
As a new entry it might be actually easy to upgrade.
Afterwards we might be back to the rare situation where Isabelle + AFP
fully work.
Makarius
___
isabelle-dev
