[isabelle-dev] the new "imports" semantics
lp15 at cam.ac.uk
Thu Nov 2 19:13:49 CET 2017
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.
> 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".
More information about the isabelle-dev