Stream: Isabelle/ML

Topic: pretty print bindings in LaTeX

Hanna Lachnitt (Feb 23 2024 at 22:39):

Hi everyone,

if write some ML text that contains a binding such as this:

image.png

Is there an option to pretty print it as I see it in jedit when using isabelle build? I.e., I don't want to print it as \<^typ>\<open>int\<close> but as shown in the picture.

Thank you

Last updated: May 04 2024 at 04:19 UTC