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


It seems that

@{thm foldl.simps(1)}


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

will do it.


Mathieu Giorgino

2009/3/16 Christian Doczkal <c.doczkal at>

> Hello
> 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.)
> --
> Regards
> Christian Doczkal

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