[isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

It’s nice that global theories don’t have to be qualified. But it’s a bit strange that it's forbidden to qualify them.

--lcp

> On 2 Nov 2017, at 17:21, Makarius <makarius at sketis.net> wrote:
> 
>> On 02/11/17 17:47, Lawrence Paulson wrote:
>> 
>> And I have triple checked that Probability is spelt correctly. Any hints?
> 
> Since Isabelle/f27488f47a47 you can use completion there (on the theory
> base name).
> 
> E.g. "ALi" completes "HOL-Library.AList".
> 
> 
>    Makarius