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
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
