[isabelle-dev] AFP failures

[Johannes Hölzl]

Am Dienstag, den 26.11.2013, 11:52 +0100 schrieb Jasmin Christian
Blanchette:
> 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?

Looks like Zorn's lemma is not included in HOL-Library anymore. When
Coinductive loads Zorn it is also included in the Latex document. (Zorn
uses \sqsubset in a local)

I added now Zorn to HOL-Library (isa# acb41098607a), at least
Coinductive works now.

 - Johannes