[isabelle-dev] the new "imports" semantics

[Dmitriy Traytel]

Hi Larry,

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).

Dmitriy

> 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?
> 
> Larry
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev