HuanSun (Jan 27 2022 at 14:23): HuanSun (Jan 27 2022 at 14:23):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][1] 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 syntax translation print_translation come into play in this diagram.
[![enter image description here][2]][2]
Furthermore, is there a simple example for learning this entire process?
[1]: https://isabelle.in.tum.de/doc/isar-ref.pdf
[2]: https://i.stack.imgur.com/JXDml.png
Last updated: Apr 25 2024 at 04:18 UTC