[isabelle-dev] the new "imports" semantics

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 2 17:47:45 CET 2017

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?


More information about the isabelle-dev mailing list