[isabelle] A way to write nested theories in a theory file?
My question is not about a normal usage issue, but rather a trick I would
enjoy, if ever there is one. If not, then I won't bother that much (as
that's not about normal Isar usage, that would be OK).
Some months ago, for my personal use, I started to edit a theory file
which is a summary of all Isar constructs, followed by minimalist example
instance and comments (comments like how does it relate to another
constructs, alternative constructs, and so on). Diving back to Isabelle, I
wanted to resume with this, and was reminded of issues I encountered at
I have issues with interfering constructs. Using “notepad” or “locale” is
not always OK, as some constructs are not allowed inside of a “notepad” or
“locale”. So in the theory file, all constructs appears at the same level,
and declarations interferes. I may use more complex names to avoid it, but
I quickly figured it's not readable and easily maintainable.
Please, any one know a trick to have something like multiple isolated
theories inside a single theory file?
I may use multiple files instead of a single, but I use anchors, and as
know near to nothing about TeX, I'm afraid of cross‑linking between
multiple documents and then publish the whole as a single PDF.
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and