Re: [isabelle-dev] Infinite_Set.thy

I have just checked, and this function is used nowhere in our libraries, including the AFP. Larry > On 27 Nov 2015, at 15:59, Tobias Nipkow wrote: > > I remember other people suggesting this as well, albeit not on this list. It > seems fair to me. Only the function

Re: [isabelle-dev] Infinite_Set.thy

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

[isabelle-dev] Infinite_Set.thy

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