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
