Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Private/qualified in locales

view this post on Zulip Email Gateway (Aug 22 2022 at 13:40):

From: Makarius <makarius@sketis.net>
No, this is still the canonical form. At least until the next big reform
in name space management.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 13:43):

From: Lars Hupel <hupel@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC