src/HOL/Tools/rewrite_hol_proof.ML
changeset 78447 43cbd96de418
parent 71777 3875815f5967
child 79175 04dfecb9343a