Email Gateway (Aug 19 2022 at 10:01): Email Gateway (Aug 19 2022 at 10:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I think this simple pattern can fulfil the needs:
local L‑n context L‑n
(* Isar samples goes here *)
end
Just have to not forget to properly manage all the “‑n” everywhere.
Email Gateway (Aug 19 2022 at 10:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Sorry, typo. Add “begin”:
local L‑n context L‑n begin
(* Isar samples goes here *)
end
Email Gateway (Aug 19 2022 at 10:20):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Last updated: May 06 2024 at 16:21 UTC