Email Gateway (Aug 19 2022 at 09:34): Email Gateway (Aug 19 2022 at 09:34):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 19 2022 at 09:34):From: Tobias Nipkow <nipkow@in.tum.de>
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
Email Gateway (Aug 19 2022 at 09:34):From: Alfio Martini <alfio.martini@acm.org>
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".
Email Gateway (Aug 19 2022 at 09:34):From: Tobias Nipkow <nipkow@in.tum.de>
You can read it online
http://isabelle.in.tum.de/repos/isabelle/file/48c0c3bc40dd/src/Doc/LaTeXsugar/Sugar.thy
but note that it based on TeX Snippets (search for snippets).
Tobias
Last updated: Apr 26 2024 at 16:20 UTC