I'm attempting to understand Isabelle's inner syntax engine, but I'm having problems reading Chapter 8 of the Isabelle standard reference manual. (Isar-ref or [The Isabelle/Isar Reference Manual] by Makarius Wenzel).
As seen in the diagram below, there is a general inner syntax engine described in the manual. I'm trying to figure out how this process works and where functions like
print_translation come into play in this diagram.
[![enter image description here]]
Furthermore, is there a simple example for learning this entire process?
Last updated: Dec 07 2023 at 16:21 UTC