[isabelle-dev] AFP failures

[Jasmin Christian Blanchette]

Hi all,

The AFP tests are finally back, and this revealed a series of failures related to my refactorings last week. Looking more closely at the falures, I found they were all in the LaTeX generation, which I hadn't tested locally before pushing. In most of the theories, it's the LaTeX symbol \sqsubset that causes problem, because the necessary package is not included.

Does anybody have any idea of why this suddenly pops up as an issue just because I moved a few theories around?

Jasmin