I'm writing a larger document in LaTeX, and while it is primarily in classic math notation, I want to include some interesting Isabelle/HOL snippets. So far (i.e. not very far yet :D) I've used verbatim, but verbatim has issues with ∀, ⇒, etc. I am aware of https://isabelle.in.tum.de/doc/sugar.pdf, however I do not want to typeset my whole document in Isabelle, merely a few snippets, which doesn't have to be 1:1 what isabelle sugar would produce.

I also found https://github.com/lammich/isabelle_llvm/blob/master/papers/2021_Enschede_Talk/lstisabelle.tex which looks promising but has rough edges and depends on some auto-generated isabelle tex files which give me plenty of LaTeX errors.

Is there some easy-to-use style I can just import and get pretty isabelle listings?

Main concerns are rendering unicode symbols (forall, etc) in the listings, maybe bold and/or colored keywords.

I just use

```
\usepackage{listings}
\definecolor{isarblue}{HTML}{006699}
\definecolor{isargreen}{HTML}{009966}
\lstdefinelanguage{isabelle}{%
keywords=[1]{type_synonym,datatype,fun,abbreviation,definition,proof,lemma,theorem,corollary},
keywordstyle=[1]\bfseries\color{isarblue},
keywords=[2]{where,assumes,shows,and},
keywordstyle=[2]\bfseries\color{isargreen},
keywords=[3]{if,then,else,case,of,SOME,let,in,O},
keywordstyle=[3]\color{isarblue},
}
\lstset{%
language=isabelle,
escapeinside={&}{&},
columns=fixed,
extendedchars,
basewidth={0.5em,0.45em},
basicstyle=\ttfamily,
mathescape,
}
```

Unicode symbols go inside mathescape `$`

.

You might need to fiddle around to get it typeset in a nice way though.

Last updated: Sep 25 2022 at 23:25 UTC