[isabelle-dev] AFP failures

[Makarius]

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?


 	Makarius