[isabelle-dev] the new "imports" semantics
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
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