NJ 1.09.2x as factory default!
New theorems suggested by Florian Kammueller
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj
Removal of card_insert_disjoint, which is now a default rewrite rule
New theorem disjoint_eq_subset_Compl
Removal of mask.sig and mask.sml
Removal of module Mask and datatype binding with its constructor |->