[isabelle-dev] AFP failures
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