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?
I would ask such questions on the mailing list. Probably only Makarius knows about this, and he doesn't read Zulip.
Thanks, that's a reasonable suggestion.
Last updated: Dec 07 2023 at 16:21 UTC