# Re: [isabelle] Typesetting inference rules

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

On Tuesday, April 17, 2012 at 12:41:47 (+0100), Björn Bartels wrote:
> 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.
>
> Björn

--



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