[isabelle-dev] AFP failures

Makarius makarius at sketis.net
Tue Nov 26 13:12:50 CET 2013

On Tue, 26 Nov 2013, Johannes Hölzl wrote:

> 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.

I don't understand this at all, neither the above explanation nor the 
formal changeset (with its vacuous log message).

How does the inclusion or non-inclusion of some theory affect the latex 
macro environment?


More information about the isabelle-dev mailing list