[isabelle-dev] AFP/Shivers-CFA latex document problem

Makarius makarius at sketis.net
Sat Nov 20 12:35:36 CET 2010

On Fri, 19 Nov 2010, Brian Huffman wrote:

> Fancy report-quality LaTeX syntax is supposed to be a supported feature 
> of Isabelle document generation. The incompatibility between the ulem 
> package and the development version of Isabelle is unfortunate, and 
> hopefully workarounds can be found so that users can continue to use 
> ulem and other LaTeX packages in the future.

The non-compositionality of LaTeX macro packages is well-known.  Every 
change on our side inevitably breaks someones setup -- I knew this only 
too well when embarking again on the long-standing copy/paste problem.

If anybody can tell me what is wrong on my side, I can amend that.

Yesterday I spent some hours with ulem.sty and got the impression that it 
is not fully canonical.  I did not notice that its last update is already 
10 years ago -- I have the same version from 2000-05-26.


More information about the isabelle-dev mailing list