Gergely Buday (Mar 27 2023 at 15:45): Gergely Buday (Mar 27 2023 at 15:45):The Isabelle/Isar Implementation manual on page 130 writes:
Adding to the genuine structured proof language requires profound understanding of the Isar/VM machinery, though, so this is beyond the scope of this manual.
While I do not want to add new elements to the language, I would like to understand the virtual machine well. What is the source for that? Isar source code and Makarius' PhD Thesis?
Manuel Eberl (Mar 29 2023 at 09:54):I would ask such questions on the mailing list. Probably only Makarius knows about this, and he doesn't read Zulip.
Gergely Buday (Mar 29 2023 at 14:11):Thanks, that's a reasonable suggestion.
Last updated: Dec 21 2024 at 16:20 UTC