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