[isabelle-dev] Infinite_Set.thy

[Lawrence Paulson]

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.

Larry