Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 13:11):

From: Christian Doczkal <c.doczkal@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.)
smime.p7s

view this post on Zulip Email Gateway (Aug 18 2022 at 13:11):

From: Makarius <makarius@sketis.net>
This is how it works:

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

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 13:12):

From: Le J <clej37@gmail.com>
Hello,

It seems that

@{thm foldl.simps(1)}

or

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

will do it.

Regards,

Mathieu Giorgino

Last updated: May 03 2024 at 12:27 UTC