[isabelle-dev] the new "imports" semantics

[Makarius]

On 02/11/17 19:13, Lawrence Paulson wrote:
> 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.

I have checked this again in the history, e.g. Isabelle/db1827610513.
Global theories in regular application sessions were merely a left-over
from early exploration of the possibilities. Only Probability and SPARK
were still remaining.

In NEWS of Isabelle/2c2a346cfe70 the situation is now explained as follows:


*** General ***

* 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".


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Completion supports theory header imports, using theory base name.
E.g. "Prob" is completed to "HOL-Probability.Probability".


	Makarius