Email Gateway (Aug 19 2022 at 17:23): Email Gateway (Aug 19 2022 at 17:23):From: "W. Douglas Maurer" <maurer@gwu.edu>
What is the relationship between antiquotations in ML and
antiquotations in Isabelle? The antiquotation mechanism in ML allows
you to write quoted text containing a part (the antiquotation) which
isn't quoted. The antiquotation mechanism in Isabelle appears to be
just a special kind of function whose name starts with an at-sign. I
don't see the connection. -WDMaurer
Email Gateway (Aug 19 2022 at 17:23):From: Lars Noschinski <noschinl@in.tum.de>
Isabelle has antiquotations both in ML blocks (or files) and in text
blocks. Both give you access to elements of your proof development:
types, terms, theorems, ... -- i.e. they switch to another language.
Last updated: Nov 21 2024 at 12:39 UTC