This makes sense. Many thanks!
Larry
> 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
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
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, Makarius wrote:
>
>> On 02/11/17 17:47, Lawrence Paulson wrote:
>>
>> And I have triple checked that Probability is spelt correctly. Any hint
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
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 Paulson wrote:
>
> I’ve been converting some theories from the old
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”