Discussion:
[isabelle] Private/qualified in locales
(too old to reply)
Lars Hupel
2016-07-07 15:20:17 UTC
Permalink
Raw Message
Dear list,

is there any shorter way than that to hide a fact in a locale?


context constructors begin
context begin (* two contexts for private qualifier *)

private lemma seval_correct0:
...

end
end



Cheers
Lars
Makarius
2016-07-25 13:25:36 UTC
Permalink
Raw Message
Post by Lars Hupel
is there any shorter way than that to hide a fact in a locale?
context constructors begin
context begin (* two contexts for private qualifier *)
...
end
end
No, this is still the canonical form. At least until the next big reform
in name space management.


Makarius

Loading...