Re: [isabelle] typesetting this



Dear Gergely,

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

hope this helps,

chris

On 07/01/2014 03:18 PM, Gergely Buday wrote:
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.

- Gergely





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