[isabelle] Typesetting inference rules



Hi all,

I am using the very nice Latex sugar capabilities of Isabelle for preparing documents from my theories. However, when typesetting inference rules (using mathpartir) with very long premises I have the problem that these exceed the line. This  is also mentioned as a limitation in the Latex sugar document. I am wondering if anyone knows a good workaround for this problem. Inserting latex linebreaks by using text{*...*} does not seem to work and editing the generated Latex documents is also not a very pleasant task.

Thanks in advance,
Björn




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.