[isabelle] ML antiquotations: let, note



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




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