Re: [isabelle-dev] the new "imports" semantics
This makes sense. Many thanks! Larry > On 3 Nov 2017, at 13:13, Makariuswrote: > > * 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the new "imports" semantics
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
Re: [isabelle-dev] the new "imports" semantics
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. --lcp > On 2 Nov 2017, at 17:21, Makariuswrote: > >> On 02/11/17 17:47, Lawrence Paulson wrote: >> >> And I have triple checked that Probability is spelt correctly. Any hints? > > Since Isabelle/f27488f47a47 you can use completion there (on the theory > base name). > > E.g. "ALi" completes "HOL-Library.AList". > > >Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the new "imports" semantics
On 02/11/17 17:47, Lawrence Paulson wrote: > And I have triple checked that Probability is spelt correctly. Any hints? Since Isabelle/f27488f47a47 you can use completion there (on the theory base name). E.g. "ALi" completes "HOL-Library.AList". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the new "imports" semantics
Hi Larry, in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means that you must import it without any session qualification (just like Main or Complex_Main). Dmitriy > On 2 Nov 2017, at 17:47, Lawrence Paulsonwrote: > > I’ve been converting some theories from the old pathname syntax to the new > setup. I have the line > > imports "HOL-Probability.Probability” > > but it is rejected with the message > > Bad theory import "HOL-Probability.Probability" > > If instead I import "HOL-Probability.Random_Permutations” or > "HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple > checked that Probability is spelt correctly. Any hints? > > Larry > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev