[isabelle-dev] AFP failures

Lawrence Paulson lp15 at cam.ac.uk
Tue Nov 26 12:58:29 CET 2013

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.


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.

More information about the isabelle-dev mailing list