Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2016-11-04

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
12:27 silver joined #isabelle
14:34 int-e hmm, Finite_Product_Measure.thy got moved to HOL/Analysis in RC0, breaking HOL/Probability/Fin_Map
14:47 larsrh int-e: something is broken in the distribution?
14:49 int-e in the RC, yes, Fin_Map imports Finite_Product_Measure but it's now in ../Analysis/
14:50 larsrh eek, that sounds bad
14:50 larsrh give me a moment to notify Johannes
14:55 larsrh Johannes says you should use HOL-Analysis as image, then it works
14:56 ThreeOfEight Still, this is a bug.
14:56 ThreeOfEight So thanks for reporting it.
15:16 int-e using the HOL-Analysis image is good advice though, thanks.

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary