Re: [isabelle] Warning: Usage of deprecated font command

In a nutshell, that is exactly why many people switched to the new setup about 10 years ago. 


> On 7 May 2014, at 11:47, Makarius <makarius at> wrote:
> Note that \it and \em do make a difference in practice, since they don't insert italic correction.  So {\em bad} will normally look bad, depending on the surrounding font, the correct form is \emph{good}.

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