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> a écrit:

Hi people,

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 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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.