[isabelle] Poor man's LaTeX markup for Isabelle listings
Dear Isabelle community,
I frequently need to include Isabelle source code listings in my LaTeX
documents. However I have not yet figured out how to make Isabelle's
document preparation machinery export LaTeX snippets. I know it's
possible, but I haven't had the time. Moreover I often need to deviate
from my verbatim formalisation for didactic purposes.
I'm sure this has been done before, and I'm sure one could realise a
more advanced solution by reusing parts of the *.sty files that come
with Isabelle, but anyway I quickly hacked this LaTeX package together
from scratch, which does part of the job:
If you check out https://github.com/clange/latex you may find a few more
useful LaTeX packages. In
https://github.com/clange/latex/blob/master/lstsemantic.sty#L20 you will
see that I have also tried this with the "listings" package, but gave up
quite soon, because the result didn't look nice.
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Mathematics in Computer Science Special Issue on “Enabling Domain
Experts to use Formalised Reasoning”; submission until 31 October.
This archive was generated by a fusion of
Pipermail (Mailman edition) and