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