*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 20 Dec 2012 08:07:42 +0100*In-reply-to*: <CAAPnxw3eaBNPH_CGjfYHX=s=XPhBVL1CB2PYa_WL6JOhw5sKkw@mail.gmail.com>*References*: <CAAPnxw3eaBNPH_CGjfYHX=s=XPhBVL1CB2PYa_WL6JOhw5sKkw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/17.0 Thunderbird/17.0

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! >

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

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

- Previous by Date: [isabelle] LaTeX Theorem Environments for Definitions and Proofs
- Next by Date: [isabelle] intro rule for &&&
- Previous by Thread: [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