src/HOL/equalities.ML
changeset 3362 0b268cff9344
parent 3356 9b899eb8a036
child 3384 5ef99c94e1fb