Email Gateway (Aug 18 2022 at 19:35): Email Gateway (Aug 18 2022 at 19:35):From: Björn Bartels <bbartels@cs.tu-berlin.de>
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
Email Gateway (Aug 18 2022 at 19:35):From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Björn,
Not sure whether this helps in your case, but my workaround
in similar situations is to type-set the inference rule
inside a minipage, such as
\begin{minipage}{4cm}
@{thm[mode=Rule] long_rule_in_question}
\end{minipage}
In this way you can control how the premises are stacked
on top of each other, rather than side by side. If you do not
like the centering and the margins mathpatir inserts by default,
you can try to play with switches like
\mprset{flushleft}
Best wishes,
Christian
Last updated: Apr 25 2024 at 16:19 UTC