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



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





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