src/HOL/equalities.ML
changeset 1574 5a63ab90ee8a
parent 1564 822575c737bd
child 1618 372880456b5b