Re: [isabelle] LaTeX Theorem Environments for Definitions and Proofs



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.