reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'

generate 'rec_o_map' and 'size_o_map' in size extension

made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)

generate size instances for new-style datatypes

invoke 'fp_sugar' interpretation hook on mutually recursive clique

declare 'bool' and its proxies as a datatype for SPASS-Pirate

added 'inj_map' as auxiliary BNF theorem

tuned whitespace

remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset

favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;