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. 

--lcp

> On 7 May 2014, at 11:47, Makarius <makarius at sketis.net> 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.