src/HOL/equalities.ML
changeset 4242 97601cf26262
parent 4231 a73f5a63f197
child 4306 ddbe1a9722ab