src/HOL/equalities.ML
changeset 1757 f7a573c46611
parent 1754 852093aeb0ab
child 1763 fb07e359b59f