Re: [isabelle] König's Lemma?

Hi Lars,

> does there exists a formalization of König's Lemma in Isabelle/HOL?
I have a formalisation of König's lemma where paths are modelled as coinductive lists. I have now added it to Coinductive in the AFP development branch as an example application.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.