Re: [isabelle] [isabelle-dev] thms with VERY long identifiers



On Wed, 21 Mar 2012, Florian Haftmann wrote:

Am 19.03.2012 17:29, schrieb Brian Huffman:
It seems that the numeric indexing works if you omit the double quotes:

@{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(29)}

I guess the quotes version would be

@{thm
"Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules"(29)}

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





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