src/HOL/equalities.ML
changeset 3476 1be4fee7606b
parent 3457 a8ab7c64817c
child 3724 f33e301a89f5