src/HOL/Library/Disjoint_Sets.thy
2015-12-10 paulson 2015-12-10 not_leE -> not_le_imp_less and other tidying
2015-07-16 hoelzl 2015-07-16 move disjoint sets to their own theory