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



Hello,

It seems that

@{thm foldl.simps(1)}

or

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

will do it.

Regards,

Mathieu Giorgino

2009/3/16 Christian Doczkal <c.doczkal at stud.uni-saarland.de>

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