src/HOL/Tools/rewrite_hol_proof.ML
changeset 81302 07e1e978b093
parent 80590 505f97165f52