[isabelle-dev] Unproven class relation finite_lattice_complete < countable

Makarius makarius at sketis.net
Mon Jan 7 11:54:45 CET 2013


On Sat, 29 Dec 2012, Florian Haftmann wrote:

>> So far.  I will stop for today, and I am not sure when I am able to turn
>> back on the issue.  But maybe I have found enough that the original
>> authors can comment on it.
>
> Yet an even more minimal example

I will study this a bit further ...


 	Makarius


More information about the isabelle-dev mailing list