Hi Larry, in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means that you must import it without any session qualification (just like Main or Complex_Main).
Dmitriy > On 2 Nov 2017, at 17:47, Lawrence Paulson <l...@cam.ac.uk> wrote: > > I’ve been converting some theories from the old pathname syntax to the new > setup. I have the line > > imports "HOL-Probability.Probability” > > but it is rejected with the message > > Bad theory import "HOL-Probability.Probability" > > If instead I import "HOL-Probability.Random_Permutations” or > "HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple > checked that Probability is spelt correctly. Any hints? > > Larry > > _______________________________________________ > 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
