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



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

	Florian

-- 

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

Attachment: signature.asc
Description: OpenPGP digital signature



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