Email Gateway (Aug 19 2022 at 11:03): Email Gateway (Aug 19 2022 at 11:03):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
from isabelle doc implementation it is not clear to me what the
purpose of the two ML antiquotations @{let ...} and @{note ...} is.
Grepping over Isabelle's sources reveals that those are only used in the
manual itself. Could anybody clarify?
On a related note, I did not understand the description of the special
non-ASCII braces in the same part of the manual.
cheers
chris
Email Gateway (Aug 19 2022 at 11:04):From: Makarius <makarius@sketis.net>
Maybe the following paper helps to understand the greater context:
http://www4.in.tum.de/~wenzelm/papers/Isar-SML.pdf
There are some important ideas in the paper that are still not
implemented, notably ways to have ML abstraction over @{term} or @{typ}
(for functions or let expressions), or the speculative @{rule}
antiquotation that compiles Pure rules into ML functions in the manner of
old-style LCF/HOL systems.
There are also some things from that time that are implemented, but turned
out as non-essential. One could invent some half-decent applications for
the above (some kind of formally-checked ML preprocessor programming), but
the two or three cononical application scenarious are missing.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC