Re: [isabelle] ML antiquotations: let, note



On Tue, 28 May 2013, Christian Sternagel wrote:

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.

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.