[isabelle-dev] AFP failures

[Lawrence Paulson]

Of course we don’t have any formal curation policy for the library, but Zorn's lemma is a fundamental result. Perhaps we need to think about what things are and are not allowed in the library. Deleting things will always be risky.

Larry

On 26 Nov 2013, at 11:30, Johannes Hölzl <hoelzl at in.tum.de> wrote:

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