* Local theory specification commands may have a 'private' or
'restricted' modifier to limit name space accesses to the local scope,
as provided by some context begin ... end block. For example:
context
begin
private definition ...
private definition ...
private lemma ...
lemma ...
Very nice!
I'll wait until the naming issue is settled before replacing my many
uses of hide_const (open)
A further naming suggestion:
(a) private/hidden
(b) qualified
the latter is akin to Haskell's qualified import.
cheers
chris
PS: I'm still waiting for
isabelle build -n -a
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
Tobias
smime.p7s
Description: S/MIME Cryptographic Signature
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
Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
versus old uses of Local_Theory.restore.
Local_Theory.open_target is the internal version of context begin, where
Local_Theory.close_target is end. The ML signature is now a bit more
concise form than before. It has
Hi Makarius,
thanks, this is the hint I was looking for a long time now.
I will do the replacement in the BNF package, but I don't think that I
will have time for it before the approaching release.
Dmitriy
On 07.04.2015 17:47, Makarius wrote:
Just a short note on Local_Theory.open_target
