John Hughes (Feb 04 2025 at 00:04): John Hughes (Feb 04 2025 at 00:04):I'd like to include Isabelle code into a LaTeX document (but not one produced from an Isabelle theory document!). I'd really like to be able to produce something that looks like this:
image.png
Of course, I can use screen-grabs from the interface and include things as images, but it'd be nice if they were instead able to be copy/pasted, etc.
Has anyone got a solution for doing this, and if so, can you provide a working tiny LaTeX document?
Just to clarify, I'd like to be able to type this into my latex document
\begin{ISA}
notation times (infix "⊙" 80)
lemma times_assoc:
fixes a::r and b::r and c::r
shows "(a ⊙ b) ⊙ c = a ⊙ (b ⊙ c)"
sorry
\end{ISA}
where ISA might be some other environment name, or maybe the whole thing actually use lstlisting, or something else. The key thing is that things like the circled-dot should be allowed as input in the latex document, i.e., that I can copy/paste from the source code shown in the Isabelle/jedit interface if at all possible.
Mathias Fleury (Feb 04 2025 at 06:03):https://isabelle.in.tum.de/dist/Isabelle2024/doc/sugar.pdf, section 7 snippets?
John Hughes (Feb 04 2025 at 12:04):I did my best to follow the instructions. I edited my theory file as suggested in section 7.1 of that article. The theory previously contained a "text" item and then a nonsense theorem. I changed it to include the suggested additional stuff around my nonsense theorem:
which frankly seemed unlikely as part of a theory document, since it looks like LaTeX. The result was that the theory suddenly had lots of errors, and the "build" no longer worked. Did I misunderstand something?
Fabian Huch (Feb 04 2025 at 12:46):It seems this doc is out of date as it uses old-style brackets ("{* *}"); nowadays we use cartouches ( \<open>, \<close>) which get suggested e.g. when you type a single "
John Hughes (Feb 05 2025 at 17:18):It also suggested using \raw_text ... in the theory document, when it should have been raw_text .... Once I got past those two things, life got easier.
David Wang (Feb 05 2025 at 18:55):I use this with minor changes.
It needs a find-and-replace after copying and pasting.
I don't know if there is a way to make Isabelle output a well-formatted listing
Last updated: Mar 09 2025 at 12:28 UTC