Email Gateway (Aug 18 2022 at 19:19): Email Gateway (Aug 18 2022 at 19:19):From: Brian Huffman <huffman@in.tum.de>
It seems that the numeric indexing works if you omit the double quotes:
@{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)}
Email Gateway (Aug 18 2022 at 19:20):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I guess the quotes version would be
@{thm
"Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules"(29)}
Florian
signature.asc
Email Gateway (Aug 18 2022 at 19:20):From: Makarius <makarius@sketis.net>
It is both correct according to the syntax as explained in the isar-ref manual.
The rules for quotes or non-quotes are not very difficult, if one knows them.
It is a bit like reading French, or Arabic ... -- a bit of interpolation is
required.
In the above case of ML antiquotations, I usually use the first version,
because it corresponds to what is usually written in Isar source as well. The
outer @{...} already tells that the whole thing is anti-quoted.
The second version is more like an imitation of ML string literals. It
probably stems from the old-style practice of refering to thm or const names
directly in raw ML, without the Isar context to take care of antiquotations:
e.g. former Const ("foo", _) is occasionally seen as
Const (@{const_name "foo"}, _) even though the extra quotes are redundant.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC