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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
