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

Reply via email to