[isabelle] LaTeX Theorem Environments for Definitions and Proofs

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):

datatype Nat = Z | suc Nat  (* here I think I can only use
antiquotations... *)



primrec add::"Nat => Nat => Nat"
    add01:  "add x Z = x" |
    add02:  "add x (suc y) = suc (add x y)"

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.