src/HOL/Tools/rewrite_hol_proof.ML
changeset 81997 d09524fdd40c
parent 80590 505f97165f52
equal deleted inserted replaced
81987:5dc2c98a6f16 81997:d09524fdd40c