I’ve pushed a correction to that particular problem. I’ve no time to verify that there are no further problems. Sorry again.
Larry > On 17 Mar 2015, at 17:22, Makarius <makar...@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? > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev