[isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

This makes sense. Many thanks!
Larry

> On 3 Nov 2017, at 13:13, Makarius <makarius at sketis.net> wrote:
> 
> * Only the most fundamental theory names are global, usually the entry
> points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
> FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
> formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171103/6eaf2eb7/attachment-0002.html>