Re: [isabelle] Displaying some element of a list of facts



On Mon, 16 Mar 2009, Christian Doczkal wrote:

> 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.

This is how it works:

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


	Makarius





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