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

  @{thm[mode=Rule] long_rule_in_question}

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


Best wishes,

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.
 > Thanks in advance,
 > Björn


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