Email Gateway (Jun 02 2022 at 10:05): Email Gateway (Jun 02 2022 at 10:05):From: Asta Halkjær From <andro.from@gmail.com>
Hi everyone,
I have developed a tool to easily include snippets of Isabelle code in
LaTeX papers.
It runs entirely in the browser and is available on my homepage:
https://people.compute.dtu.dk/ahfrom/snips/
It takes as input the LaTeX that Isabelle can already export and divides it
into small segments.
This makes it easy to include just a single definition, two lines of a
proof, a theorem statement, etc. in a paper.
More precisely, the tool defines commands for every cartouche and for every
line in the theory and tries to give these suitable names.
The user can then choose what to include in the LaTeX document. This also
works on collaborative sites like Overleaf.
The webpage includes a few examples and some useful LaTeX code to accompany
the tool.
I have used the tool for several papers myself, and so have others, but the
parsing of the exported LaTeX is ad-hoc, so the output can still be
imperfect at times.
I hope the tool may be of use to you.
Best,
Asta
Last updated: Apr 19 2024 at 04:17 UTC