Re: [isabelle-dev] the new "imports" semantics

2017-11-03 Thread Lawrence Paulson 
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
> 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

2017-11-03 Thread 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
___
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

2017-11-02 Thread Lawrence Paulson 
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 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

2017-11-02 Thread Makarius 
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

2017-11-02 Thread Dmitriy Traytel 
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 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