src/HOL/equalities.ML
changeset 6833 15d6c121d75f
parent 6832 0c92ccb3c4ba
child 7127 48e235179ffb