Email Gateway (Mar 29 2023 at 15:07): Email Gateway (Mar 29 2023 at 15:07):From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
Hi there,
I can read about the Isar Virtual Machine mainly in
Markus Wenzel. *Isabelle/Isar --- a versatile environment for
human-readable formal proof documents*
<https://mediatum.ub.tum.de/doc/601724/601724.pdf>, PhD thesis, Institut
für Informatik, Technische Universität München, 2002.
https://mediatum.ub.tum.de/doc/601724/601724.pdf
On page 50 at "Interpreting commands" it sets the semantics of the proof
commands by giving a list of low-level primitives for each command that are
sequentially executed.
I tried to find the adequate ML definitions in the src/Pure/Isar directory
but it seems that there is no one-to-one correspondence between the above
description and the ML functions. How is that semantics defined in the
source code?
My goal is not to change anything here but to understand what is going on.
Last updated: Apr 20 2024 at 12:26 UTC