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

[Florian Haftmann]

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…

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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