[isabelle-dev] Infinite_Set.thy

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 27 16:11:03 CET 2015

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.


More information about the isabelle-dev mailing list