partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;

multiset operations are defined with lift_definitions; tuned proofs;

remove outdated comment

rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;

standardized ML aliases;

clarified proof_result: finish proof formally via head tr, not end_tr;

tuned;