more robust expose_proofs corresponding to register_proofs/consolidate_theory; expose_proofs of class algebra more aggresively, to ensure early export within original theory/session context;

expose derivations more thoroughly, notably for locale/class reasoning;