[isabelle] Displaying some element of a list of facts


Say I want to display only the first part of "foldl.simps" using an
antiquotation. If I use

	@{thm "foldl.simps"} 

I get both simplification rules whereas 

	@{thm "foldl.simps(1)"}

complains about fact "foldl.simps(1)" being an unknown fact. What am I
missing here? Is there an easy way to to this? (I know that these rules
are also available under a different name, but the fact I really want to
print is not an I don't want to clutter my theory.)

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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