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

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

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

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

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