[isabelle-dev] Unproven class relation finite_lattice_complete < countable

[Florian Haftmann]

> 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

> Cheers,
> 	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Base.thy
Type: application/x-extension-thy
Size: 49 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/674cbada/attachment-0008.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Countable.thy
Type: application/x-extension-thy
Size: 88 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/674cbada/attachment-0009.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Finite_Lattice.thy
Type: application/x-extension-thy
Size: 95 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/674cbada/attachment-0010.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Merge.thy
Type: application/x-extension-thy
Size: 54 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/674cbada/attachment-0011.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121229/674cbada/attachment.sig>