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