clarified expand_proof/expand_name: allow more detailed control via thm_header;
export_standard_proofs: authentic theorem names in "print" format;