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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
