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,


On 07/01/2014 03:18 PM, Gergely Buday wrote:

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.