*To*: Giampaolo Bella <giamp at dmi.unict.it>*Subject*: Re: [isabelle] proof state into latex*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sun, 2 Oct 2011 07:16:48 -0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20111001153207.Horde.I-j7Beph4B9OhxZX7mAnXzA@mbox.dmi.unict.it>*References*: <20111001153207.Horde.I-j7Beph4B9OhxZX7mAnXzA@mbox.dmi.unict.it>*Sender*: alfio.martini at gmail.com

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! On Sat, Oct 1, 2011 at 10:32 AM, Giampaolo Bella <giamp at dmi.unict.it> wrote: > 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! > -- > Giamp > > > > > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] proof state into latex***From:*Giampaolo Bella

**References**:**[isabelle] proof state into latex***From:*Giampaolo Bella

- Previous by Date: [isabelle] proof state into latex
- Next by Date: [isabelle] Aligning full_prf with proof term
- Previous by Thread: [isabelle] proof state into latex
- Next by Thread: Re: [isabelle] proof state into latex
- Cl-isabelle-users October 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list