[isabelle-dev] [isabelle] ML antiquotations: let, note

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed May 29 22:41:23 CEST 2013

Hi Christian,

> 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?

A small example:

ML {*
@{let ?f = "distinct :: 'a list ⇒ bool"}
@{term "?f [1, 2, 3 :: nat]"};

@{note foo = distinct.simps [where ?'a = "int \<times> bool"]}
@{thms foo};

A little bit clearer? ;-)

> On a related note, I did not understand the description of the special
> non-ASCII braces in the same part of the manual.

To my understanding, those braces denote logical scopes / subcontexts
similarly to { … } in Isar.

I guess these things still need some time to get commonly used…



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130529/2a61ac5f/attachment-0001.asc>

More information about the isabelle-dev mailing list