*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Thu, 20 Dec 2012 10:48:20 -0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <50D2B93E.2010308@in.tum.de>*References*: <CAAPnxw3eaBNPH_CGjfYHX=s=XPhBVL1CB2PYa_WL6JOhw5sKkw@mail.gmail.com> <50D2B93E.2010308@in.tum.de>*Sender*: alfio.martini at gmail.com

Dear Tobias, Thank you for your the remarks. My second question below is perfectly satisfied by the antiquotation @{datatype [display] xyz}, By the way, this antiquotation *is not listed* in the reference manual, section 4.2, page 64). It is very useful :-) Now I will delve into the question of labeling proofs and definitions as we do with ams theorem package. However, before going to extremes (i.e., using TeX Snippets), is there a way to get the LaTeX Sugar manual of the development version (without having to download/build the repository version)? Best! PS: Since we have now two equally important Isabelle Tutorials, I humbly suggest naming the bulky one "LNCS Isabelle Tutorial" and the newest one simply by "Isabelle Tutorial". On Thu, Dec 20, 2012 at 5:07 AM, Tobias Nipkow <nipkow at in.tum.de> wrote: > There exists an antiquotation @{datatype xyz} you can try. If you want to > display actual parts of your Isabelle theory you can either include the > documentation into the theory, or you can show definitions by > antiquotations (eg > @{thm f.simps[no_vars]}) or perform some trickery described in the wiki > https://isabelle.in.tum.de/community/Generate_TeX_Snippets or in more > detail in > the development version of the LaTeX Sugar manual. > > Tobias > > Am 19/12/2012 19:28, schrieb Alfio Martini: > > Dear Isabelle Users, > > > > After using to some extent the Isabelle document preparation system I > > still don´t know how to do > > the following things: > > > > 1) To wrap a function (datatype, constant, proof, etc) definition inside > a > > theorem environment. It is crucial for > > making references throughout the text. For instance, something like the > > following (the examples > > are chosen just to convey what I would like to able to do): > > > > \text{* > > \begin{definition} > > datatype Nat = Z | suc Nat (* here I think I can only use > > antiquotations... *) > > > > \end{definition} > > *} > > > > > > .... > > > > \text{* > > \begin{example} > > primrec add::"Nat => Nat => Nat" > > where > > add01: "add x Z = x" | > > add02: "add x (suc y) = suc (add x y)" > > \end{example} > > *} > > > > 2) Most important, sometimes I want to display again a datatype > definition > > (theorems are easier) without having > > to type it again (using antiquotations, for instance), like it is done > many > > times in the LNCS tutorial, where many > > datatypes defined in Main are displayed again throughout the text!. > > > > Many Thanks! > > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs***From:*Tobias Nipkow

**References**:**[isabelle] LaTeX Theorem Environments for Definitions and Proofs***From:*Alfio Martini

**Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs***From:*Tobias Nipkow

- Previous by Date: [isabelle] Fwd: Isabelle2012 - What distribution?
- Next by Date: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Previous by Thread: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Next by Thread: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Cl-isabelle-users December 2012 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