Stream: Beginner Questions

Topic: Controlling visibility of theory content

Hanno Becker (Dec 05 2022 at 17:37):

Is there a way to control what part of a session/theory should be visible to other sessions?

Mathias Fleury (Dec 05 2022 at 17:49):

Kind of, you can hide lemmas, but it is slightly annoying, and find_thmstill sees them:

context
begin
private lemma myHiddenLemma: true
  sorry
end

Hanno Becker (Dec 05 2022 at 17:50):

Cool! Does this work for definitions, datatypes and type_synonyms as well?

Mathias Fleury (Dec 05 2022 at 17:52):

The other way is to use qualifiedwhich forces the user to write MyThy.LemmaName

Mathias Fleury (Dec 05 2022 at 17:54):

Hanno Becker said:

Cool! Does this work for definitions, datatypes and type_synonyms as well?

I don't remember, but I don't think so

Mathias Fleury (Dec 05 2022 at 17:56):

Actually according to grep, yes

Mathias Fleury (Dec 05 2022 at 17:57):

there are example for every command in the distribution (including one private datatypethat I have written :laughing: ) or in the AFP

Last updated: Nov 13 2025 at 04:27 UTC