nipkow at in.tum.de
Fri Nov 27 16:59:08 CET 2015
On 27/11/2015 16:11, Lawrence Paulson wrote:
> This theory proves a number of useful properties of infinite sets, and consequently, of finite sets. I’m wondering whether it makes sense to have this theory (a 17 KB file) in the Library when our main theory Finite_Set.thy (60 KB) is part of the standard HOL development. Of course we are all against bloat, but the separation of this material from the other material looks artificial.
I remember other people suggesting this as well, albeit not on this list. It
seems fair to me. Only the function atmost_one at the very end should go
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev