Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] typesetting this

view this post on Zulip Email Gateway (Aug 19 2022 at 15:15):

From: Gergely Buday <gbuday@gmail.com>
Hi,

neither @{subgoals} nor @{goals} typeset the value of _this_. Is there
a command that shows it? I would like to show what happens when
_assume_ is used.

view this post on Zulip Email Gateway (Aug 19 2022 at 15:16):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Gergely,

I think "this" is just a fact name (although introduced automatically).
So it should work via @{thm this}.

hope this helps,

chris

Last updated: Apr 26 2024 at 08:19 UTC