Generalisation of the "small" predicate to arbitrary sets;
Introduction of the coercion ord_of_nat :: "nat => V";
Addition of many new lemmas.