Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] proof state into latex

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!

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!

Email Gateway (Aug 18 2022 at 18:33):

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

Last updated: Nov 21 2024 at 12:39 UTC