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
somewhere else.
Tobias
Larry
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
