making parts of a theory private

[alleystoughton]

It would be nice to be able to mark parts of a theory as "private", meaning that the definitions and lemmas can be used in the rest of the theory but not from outside the theory, even if it's imported or through explicit qualification. Like with data abstraction, the private parts could be changed without breaking uses of the theory. Non-private parts should not mention private parts, although proofs of non-private lemmas would often use private lemmas. docgen could ignore the private parts.

[strub]

Isn't it the purpose of sections?

[alleystoughton]

Yes, at the cost of marking each private thing local. I guess that's fine.

[strub]

Why is this a cost? How would you mark things "private" in your setting?

[alleystoughton]

I was thinking of

local.
...
end local.

or something like that. So all the definitions and lemmas in that scope would be tagged as local.

[alleystoughton]

Somehow I only use sections when taking advantage of declaring abstract modules. But I could start using sections for the purpose I mentioned.