[isabelle-dev] HOL-Probability broken

[Larry Paulson]

Sorry, I don’t know how that one slipped through.

I test on my own machine.
Larry

> On 17 Mar 2015, at 17:22, Makarius <makarius at sketis.net> wrote:
> 
> In Isabelle/cd945dc13bec HOL-Probability is broken:
> 
> *** Now trying to infer coercions globally.
> ***
> *** Coercion inference failed:
> *** uncomparable types in type list
> ***
> *** Cannot fulfil subtype constraints:
> ***   ??'a  <:  ereal   from function application
> ***     \<integral>\<^sup>+ x. ereal (x ^ k * exp (- x)) *
> ***                            indicator {0::??'i..} x
> ***                        \<partial>lborel =
> ***     fact k
> ***   ereal  <:  ereal   from function application
> ***     op =
> ***      (\<integral>\<^sup>+ x. ereal (x ^ k * exp (- x)) *
> ***                              indicator {0::??'h..} x
> ***                          \<partial>lborel)
> ***   nat => ??'a  <:  ??'b => ??'c   from function application
> ***     fact::??'b => ??'c
> *** At command "lemma" (line 116 of "~~/src/HOL/Probability/Distributions.thy")
> 
> The problem might be an untested merge by Larry, but I did not make more detailed tests to prove that hypothesis.
> 
> What is also odd: http://isabelle.in.tum.de/reports/Isabelle does not show any activity nor results of testing.  Maybe the mira service is down?