*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] proof state into latex*From*: Giampaolo Bella <giamp at dmi.unict.it>*Date*: Sun, 02 Oct 2011 16:26:21 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAPnxw1WvDvktZpX6VmC_HTkEs6DrSaGf3Y4QKd7f+4yRKyqOg@mail.gmail.com>*References*: <20111001153207.Horde.I-j7Beph4B9OhxZX7mAnXzA@mbox.dmi.unict.it> <CAAPnxw1WvDvktZpX6VmC_HTkEs6DrSaGf3Y4QKd7f+4yRKyqOg@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H4 (5.0.8)

Swell! Thanks very much indeed. -- Giamp Quoting Alfio Martini <alfio.martini at 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! 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

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

**Re: [isabelle] proof state into latex***From:*Alfio Martini

- Previous by Date: [isabelle] Aligning full_prf with proof term
- Next by Date: [isabelle] Mutual induction in ML
- Previous by Thread: Re: [isabelle] proof state into latex
- Next by Thread: [isabelle] Aligning full_prf with proof term
- 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