Re: [isabelle] A way to write nested theories in a theory file?
I think this simple pattern can fulfil the needs:
local L‑n context L‑n
(* Isar samples goes here *)
Just have to not forget to properly manage all the “‑n” everywhere.
Le Mon, 04 Feb 2013 20:08:05 +0100, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> a écrit:
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 that time.
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
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