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

Reply via email to