Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] proof state into latex

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

From: Giampaolo Bella <giamp@dmi.unict.it>
Hi all,

is there a way to transform a proof state (or a portion, i.e. a
subgoal) into latex mechanically? So far, I used to take screenshots,
but they're not very practical.

Thanks!

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

From: Alfio Martini <alfio.martini@acm.org>
Hi Giampaolo,

It is very simple if you use antiquotations, like for instance:

@{subgoals [display,indent =10]}

You may want to take at look at the reference manual, page 41 (and the
tutorial, page 61)

Best!

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

From: Giampaolo Bella <giamp@dmi.unict.it>
Swell! Thanks very much indeed.

Last updated: Apr 18 2024 at 16:19 UTC