This makes sense. Many thanks!

> On 3 Nov 2017, at 13:13, Makarius <> 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".

isabelle-dev mailing list

Reply via email to