[isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

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