[isabelle-dev] the new "imports" semantics
traytel at inf.ethz.ch
Thu Nov 2 17:56:42 CET 2017
in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means that you must import it without any session qualification (just like Main or Complex_Main).
> On 2 Nov 2017, at 17:47, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev