[isabelle-dev] NEWS: limited name space accesses

[Makarius]

On Tue, 7 Apr 2015, Makarius wrote:

> On Tue, 7 Apr 2015, Tobias Nipkow wrote:
>>
>>  On 07/04/2015 14:37, Christian Sternagel wrote:
>> >     (b) qualified
>>
>>  That gets my vote because it expresses clearly the description Makarius
>>  gave: "name space entry that is only accessible by qualified names"
>
> It is definitely good to collect keyword candidates from other 
> well-known languages.
>
> I had "qualified" on my list of possibilities at first, but was hesitating to 
> use it, because there is yet another concept (c) that has no Isar notation so 
> far.  It is called Binding.qualified in ML and could solve problems like 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-February/msg00038.html

>  qualified lemma a: ...
>
>   lemma b (qualified c): ...
>   lemma e (qualified f!): ...

After thinking about this again, it looks like the following is feasible:

   now:

     private lemma a: ...   -- "no name space accesses"
     qualified lemma a: ...  -- "only qualified name space accesses"

   later, after the release:

     lemma x.y.a: -- "qualified 'base' name leading to mandatory accesses"

This means Binding.qualified is not involved here at all.  The second 
reform merely allows Binding.name / Binding.make with already qualified 
names.  There will be further consequences from this that we can explore 
after the release, such as Free variables with qualified names.


The 'private' / 'qualified' command above prefixes are technically already 
there, and I will just make one more round of renaming before we get onto 
the release lane.


 	Makarius