[isabelle-dev] the new "imports" semantics

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 3 14:15:23 CET 2017

This makes sense. Many thanks!

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

More information about the isabelle-dev mailing list